Bump version to 0.7.
Update sbt to 1.10.1.
Move scallion and silex to depend on jars via GitHub releases instead of cloning and compiling locally.
Tests now fork the jvm and use jvm options correctly, which also removes the relevant warning during testing.
Repair two broken tests, small improvements to congruence tactic.
Update to Scala 3.5.1. Silence warnings from scallion and other erroneous ones.
Resealed the Proof trait following a fix of the relevant compiler bug scala/scala3#19031.
Updated to Scala 3.4.2, and relevant minor syntax changes from -rewrite -source 3.4-migration.
Addition of the Congruence tactic, solving sequents by congruence closure using egraphs.
Addition of simply typed lambda calculus with top level polymorphism and inductive poylmorphic algebraic data types. Addition of tactics for typechecking and structural induction over ADTs.
Support for reconstructing proofs from file in SC-TPTP format. Support and inclusion of Goeland as a tactic. Doc in the manual.
Addition of a tactic that proves a sequent by applying a generic theorem on facts provided by the user. It can be used via by Apply(thm).on(fact1, fact2,...). Replaces cases where using Tautology was overkill.
The "draft()" option can now be used at the start of a file to skip checking proofs of theorem outside this file during development.
The "of" keyword can now be used to instantiate quantified variables in facts whose right hand side is a single universaly quantified formula. This can be combined freely with instantiation of free schematic symbols. Manual and tests update.
Expanded the Substitution rules to allow substitution under quantifiers when a statement of the form
Update to the user manual, change format to B5 and more improvements.
Introduction of local definitions, with methods witness, t.replace, t.collect, t.map and t.filter. Update of the manual, describing how those work, along with some corrections to the statement of axioms ot match LISA's presentation. Include test cases using each, and proved some required theorems. Fix an error in the reconstruction of OL-normalized formulas used in some tactics.
Re-added discovery of formulas which could not be substituted for error reporting to Substitution.ApplyRules
Upgrade to Scala 3.3.1
- the
Proofclass has been temporarily unsealed, till lampepfl/dotty#19031 / epfl-lara/lisa#190 is fixed - minor fixes to address compilation errors, mostly involving explicitly specifying types or implicits in some places.
Creation of the present Change Liste, going back to October 2023
Small improvement to Tableau tactics. It now uses sa weight-base heuristic for picking substitution and performs better.
- Rename some FOL classes using the word "Atomics". For example, "SchematicVarOrPredLabel" --> "SchematicAtomicLabel". This does not change any functionality.
- Improved the logic in the front's FOL. Labels are no more contravariant in their type argument; Vars and constants are no longer extending
Label[Seq[Term] |-> Term]. Apply paterns on Variables, Constants, Terms and Formulas should be cleaner and simpler. Some traits gained type parameters. - Removed the match type for
T\*\*\*N, which was used to obtain function application with arbitrary but fixed number of parameters given by N. Instead,T\*\*Nis now an opaque type forSeq[Term]. Function application withNarguments is obtained through extension methods (one for each N, not one for each implementation of (T ** N) |-> S). That's a bit less general, but more flexible and possibly more efficient. - Generally refactored the Common.scala file, ensuring uniformity across definitions. Uses less top-notch, scala-specific features and should be a bit more stable and easier to understand.
Improvements and bug fix for the Tableau tactic.
- Occur check in unification in the tableau prover made it impossible to solve formulas such as $ \forall x. D(x) \land \neg D(f(x)) $. Now variables in positive literals are renamed before unification, and mapped back after.
- The order of dependence of variables between each other is now tracked, so that when a substitution is decided, the outermost variable is instantiated first.
- New test cases that rely on these behaviours.
Reafactor and reorganize files:
-
Root project moved to lisa-sets
-
Removed unused legacy files and tests
-
Put all automation tools in the same place (lisa-sets/automation)
-
Generally flatten folder structure, when possible
-
Clean some files and imports
- Added references to publications.
- Formatted the README file generally
- Fixed grammar or spelling errors
- Make instructions a bit more explicit
- Added a tool to serialize kernel proofs. Theorems can be serialized to binary files and loaded back on later run.
- Test suite for serialization.
- On personal machine, running everything up to Recursion.scala takes 19s instead of 24s.
- Complete documentation of WithTheorems.scala
- Fixed an indexing bug in
ShrinkProof.flattenProof
- Fix typo in the Zermelo axioms in the manual.
- Pretty printing of front formulas, with infix. Printing should essentially always be valid code that can be copied back to a lisa file.
- Fix and improve extractor paterns of function and predicate symbols.
- It is now possible to return an
InvalidProofTacticresult inside aTacticSubproof. This was not possible because it is a non-local return, but some inlining makes it possible. - Fix an unsoundness error in kernel proof checker related to steps with multiple premises.
Implement a tableau based tactic for first order logic.
It can be used via by Tableau. It replaced lengthier proof scripts in most of the Quantifier.scala proofs.
It should be complete, and is not super optimized but does contains some important optimizations.
Also contains a set of dedicated tests.
Big update to the manual. It now has a "Quick Guide" section explaining how to use LISA. Also contains general corrections and clean and uniform framing for code, with support for unicode in listings.