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

Tableau (#181)

* 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
parent 49d235fe
No related branches found
No related tags found
No related merge requests found
Showing
with 484 additions and 425 deletions
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment