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

Natural deduction #10

Closed RichardMoot closed 9 years ago

RichardMoot commented 9 years ago

Important changes to sequent proof generation: more consistent propagation of atom identifiers, which will be an important step towards simpler natural deduction proof generation. Merged progress to main branch.