lisa
lisa copied to clipboard
epfl-lara
Proof assistant based on first-order logic and set theory
A comment here mentions that the type alias is equivalent, but there seems to be some weird casting happening in the background. https://github.com/epfl-lara/lisa/blob/657acdde3aac6f6c52af545238d89c19c3e1e396/lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala#L26 Consider the following: ```scala val testThm =...
Certain tactics and steps rely on external imports, but these operations will not produce sequents with assumptions. Consider for example: ```scala // over yonder val ab = have(A |- B)...
Failed `require`s currently give rather unhelpful errors. Eg: ```scala val x = variable val y = variable val g = function(2) val Z = LambdaTermTerm(Seq(x), g(x, y)) // notice this...
Error when parsing a statement or formula look like "Caused by: lisa.utils.Parser$ParserException: Unexpected input: ) ", lost in the stack trace. We should instead print meaningfull error messages before making...
This severely limits the IDE's functionality, including running and debugging code. This is because 1. `scallion` (which is a source dependency of LISA) has a `benchmark` subproject which contains outdated...
Using Eisbach tactic language of Isabelle ( https://trustworthy.systems/projects/TS/tactics ) develop a tactic to check kernel proofs in Isabelle/FOL printed using updated version of Isabelle printer.
We need to extend our test classes, in particular for the logical kernel. Some features, such as schematic symbols, are only minimally tested.
- Added a function that converts ACE input to a TPTP formula using the Attempto webservice. - Added a function that converts a TPTP formula to natural language. - Added...
- Resealed the `Proof` trait following the fix of the compiler bug causing #190 - This required upgrading to Scala >= 3.4.1 - Upgraded to 3.4.2 - There were a...
Small bug fixes to tests and minor improvements to egraph/congruence tactic.