Corrected eroneous proof. Created VariableFormulaLabel to replace arity-0 predicate schemas.
Any work on top of current LISA release should be easily adaptable by: - Changing all instances of Arity 0 SchematicFunctionLabel by VariableLabel - Changing all instances of Arity 0 SchematicPredicateLabel by VariableFormulaLabel - Changing all matching on SchematicFunctionLabel by either VariableLabel, SchematicFunctionLabel or SchematicTermLabel, according to whether the arity should be =0, >0 or >=0. - Changing all instances of multiary SchematicPredicateLabel by SchematicNPredicateLabel - Removing the empty parenthesis () that where used to transform an Arity 0 label to a term or formula. Variables have the implicit conversion without the call.
Showing
- lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala 13 additions, 1 deletion.../main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
- lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala 1 addition, 2 deletions...kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
- lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala 3 additions, 1 deletion...src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
- lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala 1 addition, 1 deletion...ries/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
- lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala 1 addition, 1 deletion...ies/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
- lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala 1 addition, 0 deletionslisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
- lisa-utils/src/main/scala/lisa/utils/Printer.scala 1 addition, 1 deletionlisa-utils/src/main/scala/lisa/utils/Printer.scala
- lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala 1 addition, 1 deletion...ils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
- src/main/scala/lisa/proven/mathematics/Mapping.scala 14 additions, 15 deletionssrc/main/scala/lisa/proven/mathematics/Mapping.scala
- src/main/scala/lisa/proven/mathematics/SetTheory.scala 9 additions, 9 deletionssrc/main/scala/lisa/proven/mathematics/SetTheory.scala
- src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala 1 addition, 1 deletion...scala/lisa/proven/tactics/SimplePropositionalSolver.scala
Loading
Please register or sign in to comment