%% File: examples.pro %% Some simple propositional linear logic formulas. Not all are %% theorems of linear logic. formula(1, a -> a). formula(2, a -> b -> a x b). formula(3, a => bang(a)). formula(4, a & b -> a & b). formula(5, a => a & a). formula(6, a => a x a). formula(7, a & b -> a). formula(8, a -> a & a). formula(9, a => b => bang(a & b)). formula(10, a & b => bang(a) x bang(b)). formula(11, (a -> b -> c) -> (a => b => c)). formula(12, (a x b -> c) -> (a -> b -> c)). formula(13, a -> b -> a x erase). formula(14, a -> b -> erase x a). formula(15, a -> b -> b x erase x a). formula(16, a -> b => b x erase x a). formula(17, (a & b) -> (a & b) -> (a x a) & (a x b) & (b x b)). formula(18, a => b -> b x bang(a)). formula(19, a => b -> bang(a) x b). formula(20, a -> a x a). formula(21, a -> a -> a). formula(22, a -> b -> a & b). formula(23, a & b -> a x 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 -> erase). test(N) :- formula(N,F), prove(nil, nil, F). % To use these examples, load both llinterp.pro and this file. % The query ?- test(N). will show that the formulas % 20, 21, 22, 23, 24 are not provable, that 17 has eight proofs, % and that 25 has two proofs.