-
- Downloads
Save proofs (#187)
-Add ids to terms like for formulas -Add serialization of proofs. Theorems can be serialized to binary files and loaded back on later run. -On my machine, running everything up to Recursion.scala takes 19s instead of 24s. -Does no hash consing, but simple optimizations to proof size (remove consecutive rewrites, flatten subproofs) -Cleans up the distinction between fullName (with the whole path, should be unique) and name (just the last part, possibly duplicate across different files/domains). -Good completion of documentation in WithTheorems -checkProofs does not print proofs of more thant 100 steps now. -fixed an indexing bug in ShrinkProof.flattenProof -Suite of tests for serialization, export then load a collection of theorems. -Push suite of tests for Tableaux tactic that were missing.
Showing
- lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala 1 addition, 1 deletion...el/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
- lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala 8 additions, 0 deletions...rnel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
- lisa-utils/src/main/scala/lisa/prooflib/BasicMain.scala 4 additions, 0 deletionslisa-utils/src/main/scala/lisa/prooflib/BasicMain.scala
- lisa-utils/src/main/scala/lisa/prooflib/Library.scala 2 additions, 0 deletionslisa-utils/src/main/scala/lisa/prooflib/Library.scala
- lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala 17 additions, 25 deletionslisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
- lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala 261 additions, 23 deletionslisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
- lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala 5 additions, 1 deletionlisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
- lisa-utils/src/main/scala/lisa/utils/LisaException.scala 3 additions, 0 deletionslisa-utils/src/main/scala/lisa/utils/LisaException.scala
- lisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala 6 additions, 5 deletionslisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala
- lisa-utils/src/main/scala/lisa/utils/Serialization.scala 721 additions, 0 deletionslisa-utils/src/main/scala/lisa/utils/Serialization.scala
- lisa-utils/src/test/scala/lisa/test/utils/ProofTacticTestLib.scala 1 addition, 1 deletion...s/src/test/scala/lisa/test/utils/ProofTacticTestLib.scala
- src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala 0 additions, 1 deletionsrc/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
- src/main/scala/lisa/settheory/SetTheoryZAxioms.scala 9 additions, 9 deletionssrc/main/scala/lisa/settheory/SetTheoryZAxioms.scala
- src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala 0 additions, 1 deletionsrc/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
- src/test/scala/lisa/automation/TableauTest.scala 130 additions, 0 deletionssrc/test/scala/lisa/automation/TableauTest.scala
- src/test/scala/lisa/utilities/SerializationTest.scala 187 additions, 0 deletionssrc/test/scala/lisa/utilities/SerializationTest.scala
Loading
Please register or sign in to comment