lisa
lisa copied to clipboard
epfl-lara
Proof assistant based on first-order logic and set theory
Slimmed down SetTheory a bit, should make it easier to find theorems. For reviewing: The first commit is moving existing things to the new package, the following commits are newly...
A small set of maintenance changes: - updated sbt version - updated Scala version - updated sbt plugin versions - slightly cleaned up sbt build - expose `lisa-sets` main classes...
The following code snippet causes a `NullPointerException`. ``` scala object A extends lisa.Main{ val f = x === x val x = variable } object C extends lisa.Main { A.x...
```scala val f = function[1] val x = variable val y = variable val P = formulaVariable val Q = predicate[1] val thm6 = Theorem(() |- ()) { val s1...
```scala val A = variable val B = variable val app = function[2] val f = variable val g = variable val x = variable val y = variable val...
Finishing up proofs about inclusion orders, on ordinals and otherwise. WIP
This pull request adds the following files: - `lisa-utils`: - `ProofsConverter.scala`: methods to transform kernel proofs to Lisa code proofs - `RunSolver.scala`: a class to run a solver for a...
New: Issue below was "fixed" by unsealing the `Proof` class. This should be reversed ASAP. But, this relies on the core pattern matching problem bring fixed in dotty. Old: **Unable...
Definitions and theorem about group theory, done in the context of set theory as part of a Bachelor project. This is a draft PR to show progress (no intent to...
