%====================================================================== %----This outputs TPTP problem clauses and formulae in a format %----acceptable to the leanCoP system (www.leancop.de). %---- %----Written by Jens Otten, November 2000 %----Extended to handle first-order: Jens Otten, June 2004 %----Modified to work with TPTP 3.x: Thomas Raths, November 2005 %====================================================================== %---------------------------------------------------------------------- %----Print out a literal with '-' for negative, nothing for positive. %----Use positive representation output_leancop_signed_literal(--('$tptp_equal'(X,Y))) :- !, write(' (equal('), write(X), write(' , '), write(Y), write('))'). output_leancop_signed_literal(--('$tptp_not_equal'(X,Y))) :- !, write(' - (equal('), write(X), write(' , '), write(Y), write('))'). output_leancop_signed_literal(++('$tptp_equal'(X,Y))) :- !, write(' - (equal('), write(X), write(' , '), write(Y), write('))'). output_leancop_signed_literal(++('$tptp_not_equal'(X,Y))) :- !, write(' (equal('), write(X), write(' , '), write(Y), write('))'). output_leancop_signed_literal(--Atom) :- !, write(' '), write(Atom). output_leancop_signed_literal(++Atom) :- write('-'), write(Atom). %---------------------------------------------------------------------- %----Print out the literals of a clause in leanCoP format. %----Special case of an empty clause output_leancop_literals([]):- write('[]'). output_leancop_literals([OneLiteral]):- !, output_leancop_signed_literal(OneLiteral). output_leancop_literals([FirstLiteral|RestOfLiterals]):- output_leancop_signed_literal(FirstLiteral), write(' ,'), nl, write(' '), output_leancop_literals(RestOfLiterals). %---------------------------------------------------------------------- %----Print out the clauses in leanCoP format. output_leancop_clauses([]). %%% for TPTP-v3.1.0 or later: %%% if clause = $true (or -($false)), then ignore it %%% if clause = $false (or -($true)), then clause set is valid and %%% the clauses [truexxx] and [-(truexxx)] are added %%% for TPTP-v3.2.0: '$true', '$false'; for TPTP-v3.1.0: $true, $false output_leancop_clauses([cnf(_Name,_Status,[Literal])|RestOfClauses]) :- (Literal = ++('$true'); Literal = ++($true); Literal = --('$false'); Literal = --($false)), !, output_leancop_clauses(RestOfClauses). output_leancop_clauses([cnf(Name,Status,[Literal])|RestOfClauses]) :- (Literal = ++('$false'); Literal = ++($false); Literal = --('$true'); Literal = --($true)), !, write('% '), write(Name), write(', '), write(Status), write('.'), nl, write('[truexxx], [-(truexxx)]'), (RestOfClauses\==[] -> (nl, nl, write(' ,'), nl, nl); true), output_leancop_clauses(RestOfClauses). output_leancop_clauses([cnf(Name,Status,Literals)|RestOfClauses]) :- write('% '), write(Name), write(', '), write(Status), write('.'), nl, write('['), output_leancop_literals(Literals), write(']'), (RestOfClauses\==[] -> (nl, nl, write(' ,'), nl, nl); true), output_leancop_clauses(RestOfClauses). %%% for TPTP-v2.7.0 or earlier: output_leancop_clauses([input_clause(Name,Status,Literals)|RestOfClauses]) :- output_leancop_clauses([cnf(Name,Status,Literals)|RestOfClauses]). %---------------------------------------------------------------------- %----Print the list of input clauses as a formula in leanCoP format. output_leancop_formula([]) :- !. output_leancop_formula(Clauses) :- nl, write('f(['), nl, nl, output_leancop_clauses(Clauses), nl, nl, write(']).'), nl, nl. %---------------------------------------------------------------------- %----Print out the connectives, quantifiers, and literals of a formula %----in leanCoP format. output_leancop_fof((~ A)) :- !, write('( ~ '), output_leancop_fof(A), write(' )'). output_leancop_fof('|'(A,B)) :- !, write('( '), output_leancop_fof(A), write(' ; '), output_leancop_fof(B), write(' )'). output_leancop_fof((A;B)) :- !, write('( '), output_leancop_fof(A), write(' ; '), output_leancop_fof(B), write(' )'). output_leancop_fof((A & B)) :- !, write('( '), output_leancop_fof(A), write(' , '), output_leancop_fof(B), write(' )'). output_leancop_fof((A => B)) :- !, write('( '), output_leancop_fof(A), write(' => '), output_leancop_fof(B), write(' )'). output_leancop_fof((A <=> B)) :- !, write('( '), output_leancop_fof(A), write(' <=> '), output_leancop_fof(B), write(' )'). output_leancop_fof((! [] : A)) :- !, output_leancop_fof(A). output_leancop_fof((! [V|L] : A)) :- !, write('( all '), print(V), write(' : '), output_leancop_fof(! L : A), write(' )'). output_leancop_fof((? [] : A)):- !, output_leancop_fof(A). output_leancop_fof((? [V|L] : A)) :- !, write('( ex '), print(V), write(' : '), output_leancop_fof(? L : A), write(' )'). output_leancop_fof('$true') :- !, write('(true___=>true___)'). output_leancop_fof($true) :- !, write('(true___=>true___)'). output_leancop_fof('$false') :- !, write('(false___ , ~ false___)'). output_leancop_fof($false) :- !, write('(false___ , ~ false___)'). output_leancop_fof('$tptp_equal'(X,Y)) :- !, write('equal('), write(X), write(' , '), write(Y), write(')'). output_leancop_fof('$tptp_not_equal'(X,Y)) :- !, write('(~ ( equal('), write(X), write(' , '), write(Y), write(')))'). output_leancop_fof(Atom) :- print(Atom). %---------------------------------------------------------------------- %----Print out the formulae in leanCoP format. output_leancop_fo_formulae([]). output_leancop_fo_formulae([fof(Name,Status,Formula)|RestOfFormulae]) :- (Status==conjecture, RestOfFormulae \= []) -> (append(RestOfFormulae,[fof(Name,Status,Formula)],Formulae), output_leancop_fo_formulae(Formulae)) ; (write('% '), write(Name), write(', '), write(Status), write('.'), nl, write('('), output_leancop_fof(Formula), write(')'), (RestOfFormulae == [] -> true; (((RestOfFormulae=[fof(_,conjecture,_)] -> (nl, nl, write(' =>'), nl, nl)); (nl, nl, write(' ,'), nl, nl)), output_leancop_fo_formulae(RestOfFormulae)))). %%% for TPTP-v2.7.0 or earlier: output_leancop_fo_formulae([input_formula(Name,Status,Fml)|RestOfFml]) :- output_leancop_fo_formulae([fof(Name,Status,Fml)|RestOfFml]). %---------------------------------------------------------------------- %----Print out the list of input formulae as a first-order formula in %----leanCoP format. output_leancop_fo_formula([]) :- !. output_leancop_fo_formula(Formulae) :- nl, write('f(('), nl, nl, %%%% Negate problems without conjecture (for CASC) (\+ (member(fof(_,conjecture,_),Formulae); member(input_formula(_,conjecture,_),Formulae)) -> (write('~ ('), nl) ; %%%% T.R. (NEGATED) (nl,write('%----This is the conjecture with negated conjecture'),nl)), output_leancop_fo_formulae(Formulae), nl, nl, (\+ (member(fof(_,conjecture,_),Formulae); member(input_formula(_,conjecture,_),Formulae)) -> (write(')'), nl); true), write(')).'), nl, nl. %---------------------------------------------------------------------- %----Print out all the clauses in leanCoP format. leancop(leancop,Clauses,_) :- tptp_clauses(Clauses), output_leancop_formula(Clauses). %---------------------------------------------------------------------- %----Print out first-order formula in leanCoP format. leancop(leancop,Formulae,_) :- tptp_formulae(Formulae), output_leancop_fo_formula(Formulae). %---------------------------------------------------------------------- %----Provide information about the leanCoP format. leancop_format_information('%','.leancop'). %---------------------------------------------------------------------- %----Provide information about the TPTP file. leancop_file_information(format,leancop). %----------------------------------------------------------------------