kdrag.solvers.ljt.prove

kdrag.solvers.ljt.prove(goal: BoolRef) → tuple[bool, list]

Prove goal intuitionistically using Dyckhoff’s LJT calculus.

>>> a,b,c,d = smt.Bools('a b c d')
>>> Not, Or, Implies, And = smt.Not, smt.Or, smt.Implies, smt.And
>>> prove(smt.Not(a))[0]
False
>>> prove(a)[0]
False
>>> prove(smt.Implies(a, a))[0]
True
>>> prove(smt.Or(a, smt.Not(a)))[0] # excluded middle
False
>>> prove(smt.Not(Not(Or(a, Not(a)))))[0]
True
>>> prove(smt.Implies(a, Implies(b, a)))[0]
True
>>> prove(smt.Implies(And(a, b), And(b, a)))[0]
True
>>> prove(smt.Implies(And(a, b), a))[0]
True
>>> prove(smt.Implies(Implies(Implies(a, b), a), a))[0] # pierce's law
False
>>> prove(smt.Not(Not(Implies(Implies(Implies(a, b), a), a))))[0]
True

Parameters:

goal (BoolRef)

Return type:

tuple[bool, list]