search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

New first-order examples #76

Open chaudhuri opened 7 years ago

chaudhuri commented 7 years ago

Some new examples have been proposed for natural numbers, addition, commutativity, etc. by @lambdacalculator.

kyagrd commented 7 years ago

Not a first order example but I've recently been working on formalizations of Intruder Deduction and Observer Theory and related proofs of some basic lemmas on consistency of the theories, which I can soon contribute as an example when the issue #77 gets resolved :) I think I've hit another bug.

chaudhuri commented 7 years ago

Great! Will look at #77 right away since the CADE deadline got moved by a week.

amerikan commented 5 years ago

@chaudhuri will you consider changing the Github issue label from just text to possibly documentation. I think it would be more meaningful.