% Theorem prover for propositional Dummett logic LC % i.e. Intuitionistic logic plus (A->B)v(B->A) % Written by Roy Dyckhoff, Summer 1998 % runs under SICSTUS Prolog % for other Prologs, maybe a different way of timing is required % and maybe "append" needs to be defined explicitly. % Incorporates ideas to avoid duplications, % based on the Vorob'ev-Hudelmaier etc calculus (I call it LJT) % See RD's paper in JSL 1992: % "Contraction-free calculi for intuitionistic logic" % and Avellone, Ferrari and Miglioli (in Milano) % Technical Report in 1997 on duplication-free sequent calculi % for various intermediate logics % and a paper by RD on making all the rules invertible. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% A is formula to prove% Time is in millisectime( A, Time ) :-statistics(runtime, _),prove(A,Result),statistics(runtime, [ _, Time]),write(Result),nl.prove( A,true ) :-provable(A), !.prove( _,false ).%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% SYNTAX%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Use of LWB concrete syntax% provided that one uses bracketmode "full":- op(425, fx, ~ ).:- op(450, yfx, & ). % left associative:- op(450, yfx, v ). % left associative:- op(500, xfx, <-> ). % non associative:- op(500, xfy, ->). % right associative%%% WARNING, this overwrites Prolog's ->% e.g. formulae look like ((a & b ) -> c) -> false, ~(~( a v (~a)))% where a,b,c etc are atoms% all atoms MUST (for internal use) be converted to the form pv(X) for some X% inspv(A, NewA) ensures that NewA has all the atoms with pv/1 as an% explicit constructor, making the clauses more deterministic% it also eliminates instances of <-> and ~.inspv( A v B, A1 v B1) :- !,inspv(A, A1), inspv(B, B1).inspv( A & B, A1 & B1) :- !,inspv(A, A1), inspv(B, B1).inspv( A -> B, A1 -> B1) :- !,inspv(A, A1), inspv(B, B1).inspv( A<->B, (A1->B1)&(B1->A1) ) :- !, % removes instance of <->inspv(A, A1), inspv(B, B1).inspv( ~A , A1->false ) :- !, % removes instance of negationinspv(A, A1).inspv( true, true ) :- !. % true not an atominspv( false, false ) :- !. % false not an atominspv( A, pv(A) ). % when all else fails% ===============================% select(List, Element, Remainder)select( [X | L], X, L).select( [Y | L], X, [Y | M]) :-select(L,X, M).on( A, [ A | _ ] ).on( A, [ _ | Rest] ) :- on(A, Rest)./*append( [], L, L ).append( [ H | T], L, [ H | TL] ) :-append(T, L, TL).*/%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% MAIN PROGRAM%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ==============================provable( A ) :-inspv(A, A1),mkempty(Left),mkempty(Right),add(A1, Right, NewRight),reduce( Left, NewRight ).reduce( Left, Right ) :-get(Left, A, NewLeft),reduce1(A, NewLeft, Right ).reduce( Left, Right ) :-reduced(Left), % avoids a cut in clause 1 for reduce/2get(Right, A, NewRight),reduce2(A, Left, NewRight).reduce( Left, Right ) :-reduced(Left), % avoids cuts in clauses 1,2 for reduce/2reduced(Right),get_imps(Right, RImps),forall(select(RImps, A->B, RestImps),reduce1(A, Left, ([], RestImps, [B]))).% Left Rules ==========================reduce1( pv(X), _, Right) :-on_atom(X, Right),!.reduce1( pv(X), Left, Right ) :-% not on_atom(X, Right),get_atom_imps(Left, X, B, Left1),add(B, Left1, Left2),add_atom(X, Left2, NewLeft),reduce(NewLeft, Right).reduce1( false, _, _).reduce1( true, Left, Right) :-reduce(Left, Right).reduce1( A v B, Left, Right) :-reduce1(A, Left, Right),reduce1(B, Left, Right).reduce1(A & B, Left, Right) :-add(B, Left, BLeft),reduce1(A, BLeft, Right).reduce1( false -> _ , Left, Right) :-reduce(Left, Right).reduce1( true -> B, Left, Right) :-reduce1(B, Left, Right).reduce1((C v D)->B, Left, Right ) :-add(D->B, Left, DBLeft),reduce1(C->B, DBLeft, Right).reduce1((C & D)->B, Left, Right ) :-reduce1(C->(D->B), Left, Right).reduce1((C->D)->B, Left, Right ) :-add(C->D, Right, CDRight),reduce1( D->B, Left, CDRight),reduce1( B, Left, Right).reduce1( pv(X) -> B, Left, Right) :-on_atom(X, Left),!,reduce1(B, Left, Right).reduce1( pv(X) -> B, Left, Right) :-% not on_atom(X, Left),add_atom_imp(X, B, Left, XBLeft),reduce(XBLeft, Right).% Right Rules =========================reduce2(pv(X), Left, _ ) :-on_atom(X, Left),!.reduce2(pv(X), Left, Right ) :-% not on_atom(X, Left)add_atom(X, Right, XRight),reduce( Left, XRight).reduce2( false, Left, Right) :-reduce(Left, Right).reduce2(true, _, _).reduce2(A & B, Left, Right ) :-reduce2(A, Left, Right),reduce2(B, Left, Right).reduce2(A v B, Left, Right ) :-add(B, Right, BRight),reduce2(A, Left, BRight).reduce2(A->B, Left, Right ) :-add_imp(A->B, Right, ABRight),reduce(Left, ABRight).% UTILITIES%=================% Sequents are represented by the pairs Left, Right% Left is a triple (Atoms, AtomImps, Ant)% Atoms is a list (unsorted) of terms X% AtomsImps is a sorted list of pairs (X,B)% Ant is the list of unprocessed formulae% Right is a triple (Atoms, Imps, Succ)% Atoms is a list (unsorted) of terms X% Imps is a list (unsorted) of implications A->B% Ant is the list of unprocessed formulae% constructorsmkempty( ([], [], []) ).add(A, (Atoms, Imps, Rest), (Atoms, Imps, [A | Rest]) ).add_atom(X, (LAtoms, LAImps, Ant), ( [X | LAtoms], LAImps, Ant)).add_atom_imp(X, B, (LAtoms, LAImps, Ant), (LAtoms, NLAImps, Ant)) :-insert( LAImps, X, B, NLAImps).add_imp( Imp, (RAtoms, RImps, Succ ), (RAtoms, [Imp | RImps], Succ ) ).% testson_atom( X, (Atoms, _, _) ) :- on(X, Atoms), !.% true iff X is an atom that has been processed on this side.reduced( (_, _, []) ).% a side of a sequent is 'reduced' iff the unprocessed part is empty% destructorsget_atom_imps((LAtoms, LAImps, Ant), X, B, (LAtoms, RestAImps, Ant)) :-extract(LAImps, X, B, RestAImps).get_imps( ( _, Imps, _) , Imps).get( (Atoms, Imps, [ A | Rest]), A, (Atoms, Imps, Rest) ).%------------------------------------------------------------------% Dealing with lists of atomic implications% AtomImps is an ordered list PL of pairs (X,B) where B is a formula% and pv(X) is an atom% lists PL are ordered by @< relation on first conponent% B is conjunction of formulae.% meaning( []) = true% meaning( ( Pair | Rest|) = meaning( Pair) & meaning(Rest)% meaning( (X,B) ) = pv(X) -> B% extract( AtomImps, X, B, RestImps)% called with AtomImps and X known; returns B and RestImps% thus meaning(AtomImps) == meaning(pv(X)->B) & meaning(RestImps)extract( [ ], _, true, []).extract( [ Pair | AtomImps], X, B, [ Pair | RestImps ] ) :-Pair = (X1, _),X @> X1, % still worth lookingextract(AtomImps, X, B, RestImps).extract( [ (X, B) | RestImps], X, B, RestImps). % Found itextract( AtomImps, X, true, AtomImps) :-AtomImps = [ (X1, _) | _ ],X @< X1. % gone too far% Not there, return 'true'% insert( AtomImps, X, B, AtomImps1)% where pv(X) is an atominsert( [], X, B, [ (X, B) ] ).insert( [ Pair |AtomImps], X, B, [ Pair | AtomImps2 ] ) :-Pair = (X1, _),X @> X1, % Needs to go further ininsert(AtomImps, X, B, AtomImps2).insert( [ (X, B1)|AtomImps], X, B, [(X,B&B1)|AtomImps] ). % Here!insert( [ Pair |AtomImps], X, B, [(X,B),Pair|AtomImps] ) :-Pair = (X1, _),X @< X1. % Needs to go before Pair