Skip to content
Snippets Groups Projects
Unverified Commit a1b378cd authored by SimonGuilloud's avatar SimonGuilloud Committed by GitHub
Browse files

Proof checker fix (#183)


* super condensed propositional tableau with eqChecker data

* work on princess

* Start working on princess-lisa

* Continued work on princess integration

* more tinkering

* trying some tableau implementation

* continue work on ATP

* Mostly working, problem with test 14 (with functions).

* test 14 does pass (make variables names unique)

* improvements on Tableau

* Proof production is completely correct!

* pruning implemented

* Tableau integreated as a tactic. Working on all theorems of the Quantifiers file, except for those with equality

* integrating tests

* Integrated tests

* clean some files

* scalafix, scalafmt

* fix unsoundness in Cut, LeftOr, RightAnd and RightIff proof checking. Correct Tableau prover accordingly.

* Adapt cut proof checking

* Adapt LeftOr proof checking

* Adapt RightAnd proof checking

* Adapting RightIff proof checking and better reporting

* scalafmt

* scalafix, scalafmt

---------

Co-authored-by: default avatarSankalp Gambhir <sankalp.gambhir47@gmail.com>
parent 13eb8604
No related branches found
No related tags found
No related merge requests found
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment