search

RichardMoot / LinearOne

LinearOne is a prototype theorem prover for first-order (multiplicative, intuitionistic) linear logic.
GNU Lesser General Public License v2.1
18 stars 2 forks source link

Allow complex terms #27

Closed RichardMoot closed 9 years ago

RichardMoot commented 9 years ago

The beta version allows a predicate to have only variable or constant terms. Some of the more subtle applications of first-order linear logic require complex terms. For example, the treatment of associativity and scope restrictions in my 2014 Lambek paper uses "integer-like" terms (of the forms s(X), s(s(X), etc.)

RichardMoot commented 9 years ago

Done! Still need to add a few more illustrations of the applications to ll1_grammar.pl