- Jul 19, 2022
-
-
SimonGuilloud authored
Changed the whole project to remove 0-arity schematic variables and replace them by variables. It compiles, but at least one proof doesn't go through.
-
- Jun 24, 2022
-
-
SimonGuilloud authored
Changed final class into sealed class for scala2 compiler
-
- Jun 23, 2022
-
-
Florian Cassayre authored
-
Florian Cassayre authored
-
Florian Cassayre authored
-
- Jun 17, 2022
-
-
SimonGuilloud authored
FUlly reorganised theory files. All seems functionning. Theory files now all simply have to extend proven.Main, and get every import and tool. Documentation for recent development. Adaptation of existing Set Theory proofs to the new canonical style.
-
SimonGuilloud authored
Printing, constructing theorems and all kinds of definitions, authomatic conversions, and much more.
-
SimonGuilloud authored
-
SimonGuilloud authored
-
- Jun 13, 2022
-
-
SimonGuilloud authored
-
SimonGuilloud authored
Printer file moved to utilities New organisation of helpers, new helper file for RunningTheory and their elements. Can show Justifications SCProofCheckerJudgement now contain the proof they refer to, no need to pass it explicitely along anymore. Other small changes.
-
SimonGuilloud authored
-
SimonGuilloud authored
-
SimonGuilloud authored
-
SimonGuilloud authored
-
SimonGuilloud authored
-
- Jun 11, 2022
-
-
Florian Cassayre authored
-
Katja Goltsova authored
-
Ekaterina Goltsova authored
This commit introduces the separation between Function/Predicate labels and theory symbols. Both constant and schematic function labels behave as functions, both constant and schematic predicate labels behave as predicates, but only constant function and predicate labels can be symbols in a theory. This is now expressed in the project by a marker trait TheorySymbol.
-
Katja Goltsova authored
-
Katja Goltsova authored
-
Katja Goltsova authored
-
Katja Goltsova authored
-
Katja Goltsova authored
-
- Jun 09, 2022
-
-
SimonGuilloud authored
Added scalafmt, scalafix and github ci as suggested in https://github.com/epfl-lara/lisa/pull/4/files. Code reformated.
-
SimonGuilloud authored
Corrected a bug in the equivalence checker. Due to small optimisations, part of checkForContradiction was reversing a list at one point, and expecting it not reverse at some other point. This made the check non-sufficient.
-
- May 15, 2022
-
-
SimonGuilloud authored
Correction of small error regarding function and predicate definition. Fix to missing case in printer match.
-
SimonGuilloud authored
-
SimonGuilloud authored
-
SimonGuilloud authored
-
SimonGuilloud authored
-
- Apr 24, 2022
-
-
SimonGuilloud authored
New substitution mechanism
-
SimonGuilloud authored
Finished the implementation of the new substitutions mechanism and made all existing proofs compatible, compiling and passing all tests again.
-
- Apr 22, 2022
-
-
SimonGuilloud authored
Implementation of lambda terms and formulas to represent substitution better. Cleaned up and reorganised substitutions. Making everything recompile is on its way
-
- Apr 15, 2022
-
-
SimonGuilloud authored
Multiple changes to the running theories
-
SimonGuilloud authored
-
SimonGuilloud authored
- 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.
-
- Mar 25, 2022
-
-
SimonGuilloud authored
Various corrections, new set theory development as better examples.
-
SimonGuilloud authored
- Corrected equivalence checker to deal correctly with empty disjunction (permits among other to use True and False in Rewrite) - Inconsequential change in a small helper method "bindAll" so that it doesn't sort variables - Small qol update in the function symbol definition in the running theory so that when verifying the definition of a new symbol, it checks the formulas with variables bound from left to right and from right to left. - InstFunSchema and InstPredSchema weren't extending SCProofStep - Corrected minor issues with axiom files of set theory (SetTheoryZAxioms, etc) - New file with some development of set theory, in particular theorems regarding mapping/replacement on sets and cartesian product. - Completed ElementsOfSetTheory so that it fills an actual theory. - Improvement/Correction of various "tactics".
-