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

Add support for additives #18

Open RichardMoot opened 9 years ago

RichardMoot commented 9 years ago

Add additives together with a contraction condition as proposed by Maieli.

This will be a major update/rewrite since it will complicate (at least) the axiom linking component: it will allow an atom to not be linked at all (if a plus link "erases" it) or to be linked multiple times (if it has a contraction link as a parent).