/****************************************************************
LLP Example
excerpted from Lolli example
examples/simple/examples.ll
****************************************************************/
/*
Formulas LLP can not prove (but Lolli can) are as follows:
14 (a -<> b -<> (top , a))
15 (a -<> b -<> (b , top , a))
16 (a -<> !b -<> (b , top , a))
14, 15, and 16 can not be proved
because treatment of 'top' is not complete in LLP.
*/
:- resource a/0, b/0, c/0.
main :-
formula(X, G),
G,
write(X), write(' solved'), nl,
fail.
main.
formula(1 , (a -<> a)).
formula(2 , (a -<> b -<> (a , b))).
formula(3 , (a => !a)).
formula(4 , ((a & b) -<> (a & b))).
formula(5 , (a => (a & a))).
formula(6 , (a => (a , a))).
formula(7 , ((a & b) -<> a)).
formula(8 , (a -<> (a & a))).
formula(9 , (a => b => ! ((a & b)))).
formula(10, (((a & b)) => (!a, !b))).
formula(11, ((a -<> b -<> c) -<> (a => b => c))).
formula(12, (((a , b) -<> c) -<> (a -<> b -<> c))).
formula(13, (a -<> b -<> (a , top))).
formula(14, (a -<> b -<> (top , a))).
formula(15, (a -<> b -<> (b , top , a))).
formula(16, (a -<> b => (b , top , a))).
formula(17, ((a & b) -<> (a & b) -<> ((a , a) & (a , b) & (b , b)))).
formula(18, (a => b -<> (b , !a))).
formula(19, (a => b -<> (!a , b))).
formula(20, (a -<> (a , a))).
formula(21, (a -<> a -<> a)).
formula(22, (a -<> b -<> (a & b))).
formula(23, ((a & b) -<> (a , b))).
formula(24, ((a -<> b -<> c) -<> (a -<> b) -<> a -<> c)).
formula(25, ((a -<> b -<> c) -<> (a -<> b) -<> (a -<> a -<> c))).
formula(26, (a -<> b -<> c -<> top)).
formula(27, (a -<> a -<> a -<> (a , top))).
formula(28, (a -<> b -<> c -<> (top , top))).
%
% The following is the explanation in Lolli distribution.
%
% This module tests the provability of some sample formulas of this fragment
% of Linear Logic. Not all are theorems.
% proving examples will cause each of the example clauses to be
% proved as many times as possible. Formulas 20 through 24 are not provable,
% 17 has eight proofs, 25 has two proofs, and 27 has three proofs. That
% formula 28 has only a single proof is a result of the lazy treatment of
% erasure, which is explained in the proof system shown in
% ../../papers/newio.dvi
% Sample Usage:
%
% ?- examples --o examples.
% 1 solved
% 2 solved
% 3 solved
% 4 solved
% 5 solved
% 6 solved
% 7 solved
% 8 solved
% 9 solved
% 10 solved
% 11 solved
% 12 solved
% 13 solved
% 14 solved
% 15 solved
% 16 solved
% 17 solved
% 17 solved
% 17 solved
% 17 solved
% 17 solved
% 17 solved
% 17 solved
% 17 solved
% 18 solved
% 19 solved
% 25 solved
% 25 solved
% 26 solved
% 27 solved
% 27 solved
% 27 solved
% 28 solved
% no