Translate proofs into Lambek calculus, Displacement calculus, hybrid or lambda grammar proofs.

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

Translate proofs into Lambek calculus, Displacement calculus, hybrid or lambda grammar proofs. #8

Closed RichardMoot closed 9 years ago

RichardMoot commented 9 years ago

Done for Lambek calculus, hybrid proofs and lambda grammar proofs. Next up, the Displacement calculus. Shifting that to a new issue and closing this one.