Pure Python first-order logic evaluator
from first_order import ForAll, Term
w = Term("w")
x = Term("x")
y = Term("y")
s1 = x & y
s2 = w | ~x
s3 = s1 >> s2
print(ForAll(x, s3))
# output: (∀ x: ((x & y) >> (w | ~x)))
print(s3 @ {"x": True, "y": True, "w": False})
# output: FalseFrom pypi:
pip install first-orderLatest commit:
pip install git+https://github.com/olivi-r/first-order.git#egg=first-orderThis project uses simple constructs to abstract the creation of first-order logic sentences:
&conjunction|disjunction~negation>>implication
Two special functions are required to create sentences with quantifiers:
Existsexistential quantifierForAlluniversal quantifier
from first_order import Exists, ForAll, Term
x = Term("x")
z = Term("z")
s_forall = ForAll(z, x | z)
s_exists = Exists(z, x | z)
print(s_forall @ {"x": False})
# output: False
print(s_exists @ {"x": False})
# output: TrueInterpretations can be applied to the sentence through the usage of the @ operator (as seen in previous examples), this takes a mapping from the names of terms used in the sentence and their respective values.
Unbound terms result in an error being thrown.
from first_order import Term
x = Term("x")
y = Term("y")
print((x | y) @ {"x": True})
# output:
# Traceback (most recent call last):
# ...
# KeyError: 'y'Terms attatched to quantifiers do not need to be in the interpretation (unless the same term name is used elsewhere)
from first_order import Exists, Term
x = Term("x")
y = Term("y")
print(Exists(y, x | y) @ {"x": True})
# output: True
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent