Multiple changes to the running theories:
- Theorems and Axioms are now stored with a name and can be fetched using that name. Definitions can be fetched using the symbol that they define. - When trying to convert a proof to a theorem or to get a definition, the user is returned a meaningfull error message indicating what went wrong. - Corrected an unsoundness that permitted to define a symbol in terms of an unbound variable or a schematic symbol.
parent
a310af53
No related branches found
No related tags found
Showing
- src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala 22 additions, 9 deletionssrc/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
- src/main/scala/lisa/kernel/fol/TermDefinitions.scala 11 additions, 5 deletionssrc/main/scala/lisa/kernel/fol/TermDefinitions.scala
- src/main/scala/lisa/kernel/proof/Judgement.scala 71 additions, 0 deletionssrc/main/scala/lisa/kernel/proof/Judgement.scala
- src/main/scala/lisa/kernel/proof/RunningTheory.scala 67 additions, 61 deletionssrc/main/scala/lisa/kernel/proof/RunningTheory.scala
- src/main/scala/lisa/settheory/SetTheoryDefinitions.scala 1 addition, 1 deletionsrc/main/scala/lisa/settheory/SetTheoryDefinitions.scala
- src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala 2 additions, 2 deletionssrc/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
- src/main/scala/lisa/settheory/SetTheoryZAxioms.scala 11 additions, 3 deletionssrc/main/scala/lisa/settheory/SetTheoryZAxioms.scala
- src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala 2 additions, 2 deletionssrc/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
- src/main/scala/proven/DSetTheory/Part1.scala 8 additions, 8 deletionssrc/main/scala/proven/DSetTheory/Part1.scala
- src/main/scala/proven/ElementsOfSetTheory.scala 3 additions, 4 deletionssrc/main/scala/proven/ElementsOfSetTheory.scala
- src/test/scala/lisa/proven/SimpleProverTests.scala 2 additions, 1 deletionsrc/test/scala/lisa/proven/SimpleProverTests.scala
Loading
Please register or sign in to comment