% 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 millisec
time( 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 negation
inspv(A, A1).
inspv( true, true ) :- !. % true not an atom
inspv( false, false ) :- !. % false not an atom
inspv( 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/2
get(Right, A, NewRight),
reduce2(A, Left, NewRight).
reduce( Left, Right ) :-
reduced(Left), % avoids cuts in clauses 1,2 for reduce/2
reduced(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
% constructors
mkempty( ([], [], []) ).
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 ) ).
% tests
on_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
% destructors
get_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 looking
extract(AtomImps, X, B, RestImps).
extract( [ (X, B) | RestImps], X, B, RestImps). % Found it
extract( 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 atom
insert( [], X, B, [ (X, B) ] ).
insert( [ Pair |AtomImps], X, B, [ Pair | AtomImps2 ] ) :-
Pair = (X1, _),
X @> X1, % Needs to go further in
insert(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