% version 24.03.13

:- use_module(library(readutil)).

?-op(140,fy,neg).
?-op(180, yfx, [and, or]).
?-op(200, xfy, [imp]).

is_unary(neg neg _X).
is_binary(X) :- member(X,[and, or, imp]).

is_conjunctive(_X and _Y).
is_conjunctive(neg(_X or _Y)).
is_conjunctive(neg(_X imp _Y)).

is_disjunctive(neg(_X and _Y)).
is_disjunctive(_X or _Y).
is_disjunctive(_X imp _Y).

component(neg neg X, X).
components(X and Y, X,Y).
components(neg(X and Y), neg X, neg Y).
components(X or Y,X,Y).
components(neg(X or Y), neg X, neg Y).
components(X imp Y, neg X, Y).
components(neg(X imp Y), X, neg Y).

is_universal(all(_,_)).
is_universal(neg some(_,_)).

is_existential(some(_,_)).
is_existential(neg all(_,_)).

/*   literal(X) :- X is a literal.
*/
is_literal(X) :-
	\+ is_conjunctive(X),
	\+ is_disjunctive(X),
	\+ is_unary(X),
	\+ is_universal(X),
	\+ is_existential(X).

/*   atomicfmla(X) :- X is an atomic formula.
*/
is_atomicfmla(X) :-
	is_literal(X),
	X \= neg _.

/*   sub(Term, Variable, Formula, NewFormula) :-
         NewFormula is the result of substituting
         occurrences of Term for each free
         occurrence of Variable in Formula.
*/

sub(Term, Variable, Formula, NewFormula) :-
	sub1(Term, Variable, Formula, NewFormula) , !.

sub1(Term, Var, A, Term) :- Var == A.
sub1(_Term, _Var, A, A) :- atomic(A).
sub1(_Term, _Var, A, A) :- var(A).

sub1(Term, Var, neg X, neg Y) :-
	sub1(Term, Var, X, Y).

sub1(Term, Var, Binary_One, Binary_Two) :-
	is_binary(F),
	Binary_One =.. [F, X, Y],
	Binary_Two =.. [F, U, V],
	sub1(Term, Var, X, U),
	sub1(Term, Var, Y, V).

sub1(_Term, Var, all(Var, Y), all(Var, Y)).
sub1(Term, Var, all(X, Y), all(X, Z)) :-
	sub1(Term, Var, Y, Z).
sub1(_Term, Var, some(Var, Y), some(Var, Y)).
sub1(Term, Var, some(X, Y), some(X, Z)) :-
	sub1(Term, Var, Y, Z).

sub1(Term, Var, Functor, Newfunctor) :- 
	Functor =.. [F | Arglist],
	sub_list(Term, Var, Arglist, Newarglist),
	Newfunctor =.. [F | Newarglist].

sub_list(Term, Var, [Head | Tail], [Newhead | Newtail]) :-
	sub1(Term, Var, Head, Newhead),
	sub_list(Term, Var, Tail, Newtail).

sub_list(_Term, _Var, [], []).

/*  instance(F, Term, Ins) :-
         F is a quantified formula, and Ins is the result
         of removing the quantifier and replacing all
         free occurrences of the quantified variable by
         occurrences of Term.
*/

instance(all(X,Y), Term, Z) :- sub(Term, X, Y, Z).
instance(neg some(X,Y), Term, neg Z) :- sub(Term, X, Y, Z).
instance(some(X,Y), Term, Z) :- sub(Term, X, Y, Z).
instance(neg all(X,Y), Term, neg Z) :- sub(Term, X, Y, Z).

/*   sko_fun(X, Y) :-
         X is a list of free variables, and Y is a
         previously unused Skolem function symbol
         applied to those free variables.
*/

sko_fun(Varlist, Skoterm) :-
	gensym(skofun,SkolemFS),
	Skoterm =.. [SkolemFS | Varlist].

/*   notation(Notated, Free) :-
         Notated is a notated formula, and Free is its
         associated free variable list.
*/

notation(n(X, _Y), X).

/*   fmla(Notated, Formula) :-
         Notated is a notated formula, and Formula is its
         formula part.
*/

fmla(n(_X, Y), Y).


stepCNF([C|Cs],NCs) :-
	member(NotatedFormula,C),
	notation(NotatedFormula,Free),
	fmla(NotatedFormula,Formula),
	is_unary(Formula),
	component(Formula,NewFormula),
	notation(NewNotatedFormula, Free),
	fmla(NewNotatedFormula, NewFormula),
	delete(C,NotatedFormula,NC0),
	append(NC0,[NewNotatedFormula],NC),
	append(Cs,[NC],NCs).
stepCNF([C|Cs],NCs) :-
	member(NotatedBeta,C),
	notation(NotatedBeta, Free),
	fmla(NotatedBeta, Beta),
	is_disjunctive(Beta),
	components(Beta,Beta1,Beta2),
	notation(NotatedBeta1, Free),
	fmla(NotatedBeta1, Beta1),
	notation(NotatedBeta2, Free),
	fmla(NotatedBeta2, Beta2),
	delete(C,NotatedBeta,NC0),
	append(NC0,[NotatedBeta1,NotatedBeta2],NC),
	append(Cs,[NC],NCs).
stepCNF([C|Cs],NCs) :-
	member(NotatedAlpha,C),
	notation(NotatedAlpha, Free),
	fmla(NotatedAlpha, Alpha),
	is_conjunctive(Alpha),
	components(Alpha,Alpha1,Alpha2),
	notation(NotatedAlpha1, Free),
	fmla(NotatedAlpha1, Alpha1),
	notation(NotatedAlpha2, Free),
	fmla(NotatedAlpha2, Alpha2),
	delete(C,NotatedAlpha,NC0),
	append(NC0,[NotatedAlpha1],NC1),
	append(NC0,[NotatedAlpha2],NC2),
	append(Cs,[NC1,NC2],NCs).
stepCNF([C|Cs],NCs) :-
	member(NotatedDelta,C),
	notation(NotatedDelta, Free),
	fmla(NotatedDelta, Delta),
	is_existential(Delta),
	sko_fun(Free, Term),
	instance(Delta, Term, DeltaInstance),
	notation(NotatedDeltaInstance, Free),
	fmla(NotatedDeltaInstance, DeltaInstance),
	delete(C,NotatedDelta,NC0),
	append(NC0,[NotatedDeltaInstance],NC),
	append(Cs,[NC],NCs).
stepCNF([C|Cs],NCs) :-
	member(NotatedGamma,C),
	notation(NotatedGamma, Free),
	fmla(NotatedGamma, Gamma),
	is_universal(Gamma),
	NewFree = [V | Free],
	instance(Gamma, V, GammaInstance),
	notation(NotatedGammaInstance, NewFree),	
	fmla(NotatedGammaInstance, GammaInstance),
	delete(C,NotatedGamma,NC0),
	append(NC0,[NotatedGammaInstance],NC),
	append(Cs,[NC],NCs).
stepCNF([C|Cs],[C|NCs]) :-
	stepCNF(Cs,NCs).

% tests
:-stepCNF([[n([X], neg (p(X)or neg p(X)))]],[[n([X], neg p(X))], [n([X], neg neg p(X))]]).

expand(Cs,NCs) :-
	stepCNF(Cs,Cs0),
	expand(Cs0,NCs).
expand(Cs,Cs).


clauseform(Formula,ClauseForm) :-
	reset_gensym(skofun),
	notation(NotatedFormula, [ ]),
	fmla(NotatedFormula, Formula),
	expand([[NotatedFormula]],NotatedClauses),
	clauses(NotatedClauses,ClauseForm).

clauses([NC|NCs],[C|Cs]) :-
	notatedclause(NC,C),
	clauses(NCs,Cs).
clauses([],[]).

notatedclause([NotatedLiteral|NC],[Literal|C]) :-
	fmla(NotatedLiteral,Literal),
	notatedclause(NC,C).
notatedclause([],[]).

:- clauses([[n([X], neg p(X))], [n([X], neg neg p(X))]],_Cs).
:- clauseform(neg all(X,p(X) or neg p(X)),_Cs).
:- clauseform((((((a or e) and (a or b)) and (b or c)) and (c or d)) and (d or e)) or neg (((((a or e) and (a or b)) and (b or c)) and (c or d)) and e),_X).

?-op(140,fy, [~, ?, !, neg]).
?-op(180, yfx, [&, and, or]).
?-op(180, yfx, '!=').
?-op(200, xfy, [imp, =>]).
?-op(160, xfy, :).

is_connective(Op) :-
	member(Op,[~,neg,&,and,'|',or,=>,imp]).

% translate_fmla/2 <-- translate TPTP format into internal formula format
%

translate(~,neg).
translate(&,and).
translate('|',or).
translate(=>,imp).

translate_fmla(Frm,TFrm) :-
	Frm =.. [Op|Frms],
	is_connective(Op),
	!,
	translate(Op,TOp),
	translate_fmlas(Frms,TFrms),
	TFrm =..[TOp|TFrms].
translate_fmla(Frm,all(Xs,TFrm)) :-
	Frm =.. [:,Vars,Frm0],
	Vars =.. [!,Xs],
	!,
	translate_fmla(Frm0,TFrm).
translate_fmla(Frm,some(Xs,TFrm)) :-
	Frm =.. [:,Vars,Frm0],
	Vars =.. [?,Xs],
	!,
	translate_fmla(Frm0,TFrm).
translate_fmla(Frm,Frm).

translate_fmlas([F|Fs],[TF|TFs]) :-
	translate_fmla(F,TF),
	translate_fmlas(Fs,TFs).
translate_fmlas([],[]).

% translate_clause/2 <-- translate TPTP format into internal clause format
%
translate_clause(Disjunction,[L|Cs]) :-
	Disjunction =.. ['|',L0,RestDisjunction],
	!,
	translate_fmla(L0,L),
	translate_clause(RestDisjunction,Cs).
translate_clause(Literal,[L]) :-
	translate_fmla(Literal,L).

% read_input(File,Input) <-- reads in an Input from File
% where Input is either a negated Formula, or a clause set

is_fof_annotated([fof(_,_,_)|_]).
is_cnf_annotated([cnf(_,_,_)|_]).

read_input(File,Input) :-
	read_file_to_terms(File,Problem,[]),
	is_fof_annotated(Problem),
	problem2negformula(Problem,Input).
read_input(File,Input) :-
	read_file_to_terms(File,Problem,[]),
	is_cnf_annotated(Problem),
	problem2clauses(Problem,Input).

% problem2negformula(Problem,NegatedFormula) <-- transforms a Problem 
% to a negated Formula
%
problem2negformula(Problem,NegatedFormula) :-
	is_fof_annotated(Problem),
	p2fmlas(Problem,Axioms,Conjectures),
	fmlas2formula(Axioms,Conjectures,NegatedFormula).

p2fmlas([fof(_,axiom,(Axiom0))|Problem],[Axiom1|Axioms],Conjectures) :-
	translate_fmla(Axiom0,Axiom1),
	p2fmlas(Problem,Axioms,Conjectures).
p2fmlas([fof(_,conjecture,(Conjecture0))|Problem],Axioms,[Conjecture1|Conjectures]) :-
	translate_fmla(Conjecture0,Conjecture1),
	p2fmlas(Problem,Axioms,Conjectures).
p2fmlas([],[],[]).

fmlas2formula(Axioms,Conjectures,NegatedFormula) :-
	negate_conjectures(Conjectures,NegatedConjectures),
	append(Axioms,NegatedConjectures,Frms),
	conjunctions(Frms,NegatedFormula).

negate_conjectures([C|Cs],[neg(C)|NCs]) :-
	negate_conjectures(Cs,NCs).
negate_conjectures([],[]).

conjunctions([F0,F1|Fs],F0 and Formula) :-	
	conjunctions([F1|Fs],Formula).
conjunctions([Formula],Formula).

% problem2clauses(Problem,Clauses) <-- transforms a Problem 
% to a clause set
%
problem2clauses(Problem,Clauses) :-
	is_cnf_annotated(Problem),
	p2clauses(Problem,Clauses).

p2clauses([cnf(_,Role,C0)|Problem],[C|Cs]) :-
	member(Role,[axiom,hypothesis,negated_conjecture]),
	translate_clause(C0,C),
	p2clauses(Problem,Cs).
p2clauses([],[]).

input2clauses(File,ClauseForm) :-
	read_file_to_terms(File,Problem,[]),
	is_fof_annotated(Problem),
	!,
	problem2negformula(Problem,Formula),
	clauseform(Formula,ClauseForm).
input2clauses(File,Clauses) :-
	read_file_to_terms(File,Problem,[]),
	is_cnf_annotated(Problem),
	!,
	problem2clauses(Problem,Clauses).

test(Cs1,Cs2) :-
	test2(Cs1,Cs3),
	permutation(Cs3,Cs2).

test2([],[]).
test2([C|Cs],[D|Ds]) :-
	permutation(C,D),
	test2(Cs,Ds).

dual(A, neg A) :-
	unify_with_occurs_check(A, A).
dual(neg A, A) :-
	unify_with_occurs_check(A, A).


resolvent(C,D,Resolvent) :-
	copy_term(C,C1),
	copy_term(D,D1),
	select(A,C1,C2),
	select(B,D1,D2),
	dual(A,B),
	append(C2,D2,Resolvent).

no_doubles(Xs,Ys) :-
	no_doubles(Xs,[],Ys).

no_doubles([X|Xs],Acc,Ys) :-
	member(X,Acc),
	!,
	no_doubles(Xs,Acc,Ys).
no_doubles([X|Xs],Acc,Ys) :-
	append(Acc,[X],Acc1),
	no_doubles(Xs,Acc1,Ys).
no_doubles([],Ys,Ys).

factor(C,Factor) :-
	select(A,C,Factor),
	member(B,Factor),	
	unify_with_occurs_check(A, B).

tautology(C) :-
	member(A,C),
	member(B,C),
	B == neg A.

forward_subsumption(Cs,D,C) :-
	member(D,Cs),
	subsumes(D,C).

subsumes(C,D) :-
	subclause(C1,D),
	subsumes_term(C1,C).

subclause(C,D) :-
	subsequence(C1,D),
	permutation(C,C1).

subsequence([X|Xs],[X|Ys]) :-
	subsequence(Xs,Ys).
subsequence(Xs,[_Y|Ys]) :-
	subsequence(Xs,Ys).
subsequence([],_Ys).

:- subsumes([p(a)],[p(_X),q(_Y)]).
:- \+ subsumes([r(X,X),r(Y,Y)],[r(a,a)]).
:- subclause([b,c],[a,b,c,d]).

condensation(C,D) :-
	multiple_factor(D,C),
	C \== D,
	subsumes(C,D).

multiple_factor(C,C).
multiple_factor(C,D) :-
	factor(C,C1),
	multiple_factor(C1,D).

:- condensation([r(b),p(a)],[p(_X),r(b),p(a),r(_Z)]).

resolution_step(Cs,WorkedOff,[Factor|WorkedOff],[Factor|NewCs]) :-
	select(C,Cs,NewCs),
	factor(C,Factor),
	write('factor:'), writeln(Factor).	
resolution_step(Cs,WorkedOff,[Resolvent|WorkedOff],[Resolvent|Cs]) :-
	member(C,Cs),
	member(D,Cs),
	resolvent(C,D,Resolvent),
	\+ member(Resolvent,WorkedOff),
	\+ forward_subsumption(Cs,_E,Resolvent),
	write('resolvent:'), writeln(Resolvent).

empty_clause(Cs) :-
	member([],Cs).

res_prover(Formula) :-
	clauseform(neg(Formula),ClauseForm),
	!,
	clause_prover(ClauseForm).

clause_prover(ClauseSet) :-
	no_doubles(ClauseSet,ClauseSet1),
	resolution(ClauseSet1,[],_WorkedOff,Saturation),
	empty_clause(Saturation),
	!.

reduce([C|Cs],NCs) :-
	tautology(C),
	!,
	reduce(Cs,NCs).
reduce([C|Cs],[C|NCs]) :-
	reduce(Cs,NCs).
reduce([],[]).

resolution(Cs,Ws,Ws,NCs) :-
	reduce(Cs,NCs).
resolution(Cs,Ws0,Ws,NCs) :-
	resolution_step(Cs,Ws0,Ws1,NCs1),
	!,
	resolution(NCs1,Ws1,Ws,NCs).


prover(File) :-
	input2clauses(File,Clauses),
	clause_prover(Clauses).