Intuitionistic assumei/1 adds temporarily a clause usable
in later proofs. Such a clause can be used an indefinite
number of times, mostly like asserted clauses, except that it
vanishes on backtracking.
Its scoped version Clause=>Goal or [File]=>Goal
makes Clause or the set of clauses found in File
available only during the proof of Goal. Both vanish on backracking.
Clauses are usable an indefinite number of times in the proof, i.e.
for instance ?-assumei(a(13)),a(X),a(Y) will succed.
Linear assumel/1 adds temporarily a clause usable at most once
in later proofs. This assumption also vanishes on backtracking.
Its scoped version Clause-:Goal or [File]-:Goal
makes Clause or the set of clauses found in File
available only during the proof of Goal. Both vanish on backracking.
Each clause is usable at most once in the proof, i.e.
for instance ?-assumel(a(13)),a(X),a(Y) will fail.
You can freely mix linear and intutionistic clauses and implications for the same predicate. Try out something like
?-a(10)-:a(11)=>a(12)-:a(13)=>(a(X),a(X)). X=11; X=13; no
This shows that a(10) and a(12) are consumed after their
first use while a(11) and a(13) are reusable indefinitely.
See the relatively straightforward implementation of these predicates in the file extra.pl.
Note that BinProlog's linear implication succeeds even if not all the assumptions are consumed while in systems like Lolli this is a strong requirement. Quantifiers and other linear operators are not implemented at this time, but can be added in the future if there's enough demand for them.