FormalSAT / trestle

Apache License 2.0
18 stars 2 forks source link

Commit containing verified basic SR checker. #20

Open ccodel opened 8 months ago

ccodel commented 8 months ago

Small additions to PropFun.lean, ToMathLib.lean, and ICnf.lean, particularly to reason about when literals equal each other and for entailment among clauses and formulas.

Lots of changes in Experiments/ for PPA, PS, and SRChecker.

JamesGallicchio commented 6 months ago

we should get this rebased onto latest main. do you have more changes locally?