abella
abella copied to clipboard
abella-prover
An interactive theorem prover based on lambda-tree syntax
Todd Wilson (@lambdacalculator) suggests in the Abella mailing list that we should add a `unfold named_clause with ...` form to handle cases such as: ~~~~ %:tapp: of (tapp P E)...
The issue was filed by @ThatDaleMiller here: https://github.com/abella-prover/abella-prover.org/issues/12
Abella offers a great HOAS system for PL proofs. However, projects developed in Abella seems to have much more SLOC compared with (more or less) equivalent proof written in Coq....
Some new examples have been proposed for natural numbers, addition, commutativity, etc. by @lambdacalculator.
- [ ] Abella should output XML or sexps or something that doesn't require guesswork - [ ] Need to remove the dependency on OMake. - [ ] Consider rewriting...
When you use names like `n1` and `n2` in a context relation definition case analysis on a hypotheses with an existing nominal constant dependency can end up missing a necessary...
In an earlier version of Abella, the searches in this (small) theorem completed almost instantly with the witnesses indicated in the comments. Now they hang, or at least take more...
I like the inductive restriction symbols @(equal) and *(smaller) for their simplicity. I wonder if we could make use of these symbols to prove the size of objects. For example,...
It used to take about 20 seconds to rebuild the entire examples suite prior to 2.0.6. Now it takes nearly three minutes. I've done a very light amount of profiling...
Is there a way to establish an equivalence relation (other than the structural one "=") that respects substitution? If I specify: ```eq (F X) (F Y) :- eq X Y.```...
Metadata
Owner
Metadata
An interactive theorem prover based on lambda-tree syntax