Translate proofs into Displacement calculus

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 Displacement calculus #17

Closed RichardMoot closed 9 years ago

RichardMoot commented 9 years ago

Add translation of first-order linear logic proof (natural deduction and/or sequent calculus) into Displacement calculus proofs.

RichardMoot commented 9 years ago

Made good progress of the Displacement calculus natural deduction component. The left and right projections still need some work and more testing is necessary

RichardMoot commented 9 years ago

The treatment of reflexives still needs some work (being developed in the displacement branch). However, I believe this issue to be minor enough to close the issue for now.