%============================================================================== %----This outputs in CLIF/HYBRID format %---- %----Written by Geoff Sutkiffe, March 2008 %----This mistreats constants that look like variables. %----DANGER - CONSTANTS THAT LOOK LIKE VARIABLES GET TREATED AS VARIABLES %============================================================================== %============================================================================== %----Generic output %============================================================================== %----Translate symbols if necessary. Only equal right now output_kif_symbol('$tptp_equal'):- !, write('='). output_kif_symbol('$tptp_not_equal'):- !, write('/='), print_message(warning,"ERROR - SHOULD NOT GET HERE - PLEASE TELL GEOFF"). output_kif_symbol(Reserved):- tptp2X_member(Reserved,[forall,exists,iff,implies,if,and,or,not]), !, write(Reserved), write('__kif'). %---All others do as is output_kif_symbol(Symbol):- write(Symbol). %------------------------------------------------------------------------------ %----Output an atom with variables in KIF format output_kif_term([OneTerm]):- !, output_kif_term(OneTerm). output_kif_term([FirstTerm|RestOfTerms]):- !, output_kif_term(FirstTerm), write(' '), output_kif_term(RestOfTerms). %----Variables look like atoms that start with uppercase. For KIF they %----need a leading ?. output_kif_term(Variable):- atomic(Variable), name(Variable,[FirstASCII|_]), FirstASCII >= 65, FirstASCII =< 90, !, write('?'), write(Variable). %----Numbervars variables look like shit. output_kif_term('$VAR'(Index)):- !, write('?'), write('$VAR'(Index)). %----Normal atomic things output_kif_term(Term):- atomic(Term), !, write(Term). %----Complex terms output_kif_term(Complex):- Complex =.. [Symbol|Arguments], write('('), output_kif_symbol(Symbol), write(' '), output_kif_term(Arguments), write(')'). %------------------------------------------------------------------------------ %----Output an atom kif_output_variable(Variable):- write('?'),write(Variable). %------------------------------------------------------------------------------ %----Output an atom %----Constants kif_output_atom(_,'$true'):- !, write('(or)'). kif_output_atom(_,'$false'):- !, write('(and)'). %----Propositions get ()ed kif_output_atom(_,Atom):- atomic(Atom), !, write('('), writeq(Atom), write(')'). kif_output_atom(_,Atom):- output_kif_term(Atom). %------------------------------------------------------------------------------ %============================================================================== %----FOF output %============================================================================== %------------------------------------------------------------------------------ %----Recognise and split up quantified formulae kif_quantified_formula(QuantifiedFormula,KIFQuantifier,Variables, Formula):- QuantifiedFormula =.. [:,Quantification,Formula], !, Quantification =.. [Quantifier,Variables], tptp2X_member(ct(Quantifier,KIFQuantifier),[ct('!',forall),ct('?',exists)]). %------------------------------------------------------------------------------ %----Recognise and split up binary formulae kif_binary_formula(BinaryFormula,KIFConnective,LHS,RHS):- BinaryFormula =.. [Connective,LHS,RHS], tptp2X_member((Connective)-(KIFConnective), [('<=>')-('iff'),('<~>')-('xor'),('<=')-('then'),('=>')-('if'),('&')-('and'), (';')-('or'),('|')-('or')]). %----Both needed after shorten which sets '|' somewhere - need to check %----|;BUG %------------------------------------------------------------------------------ %----Recognise and split up unary formulae kif_unary_formula(UnaryFormula,KIFConnective,Formula):- UnaryFormula =.. [Connective,Formula], %----Had to use ()s due to some Prolog confusion about - tptp2X_member((Connective)-(KIFConnective),[('~')-('not')]). %------------------------------------------------------------------------------ %----The format for outputing quantified formulae in oscar format %----FormulaPrefix,VariablesPrefix,VariablesSeparator,VariablesSuffix, %----FormulaSuffix kif_quantified_format('(',' (',' ',')',' )'). %----PrefixBracket,ConnectivePrefix,ConnectiveSuffix,SuffixBracket kif_binary_format('(','','',' )'). %----FormulaPrefix,ConnectiveSuffix,FormulaSuffix kif_unary_format('(',' ',' )'). %------------------------------------------------------------------------------ %----If the formulae has an acceptable status then output output_kif_formulae([]). output_kif_formulae([fof(Name,Role,Formula)|RestOfFormulae]):- write('(cl:comment '), write('"'), write(Name), write(', '), write(Role), write('"'), nl, %----To do by negating conjecture % (Role==conjecture -> % ( write('//----This is the conjecture with negated conjecture'), % nl, % output_generic_prefix_formula(kif,~Formula) % ) % ; output_generic_prefix_formula(kif,Formula)), output_generic_prefix_formula(kif,Formula), write(' )'), nl, nl, output_kif_formulae(RestOfFormulae). %------------------------------------------------------------------------------ output_kif_formulae_by_roles(Formulae):- tptp2X_findall_setof1(Role,tptp2X_member(fof(_,Role,_),Formulae),Roles), tptp2X_member(Role,Roles), findall(fof(Name,Role,Formula),tptp2X_member(fof(Name,Role,Formula), Formulae),FormulaeWithRole), write('(cl:text '), write(Role), nl, nl, output_kif_formulae(FormulaeWithRole), write(')'), nl, nl, fail. output_kif_formulae_by_roles(_). %------------------------------------------------------------------------------ %============================================================================== %----CNF output %============================================================================== %------------------------------------------------------------------------------ output_kif_signed_literal(++'$tptp_not_equal'(LHS,RHS)):- !, output_kif_signed_literal(--'$tptp_equal'(LHS,RHS)). output_kif_signed_literal(--Atom):- !, write('(not '), kif_output_atom(cnf,Atom), write(')'). output_kif_signed_literal(++Atom):- kif_output_atom(cnf,Atom). %------------------------------------------------------------------------------ %----Output the literals of the clause in KIF format %----Special case of an empty clause output_kif_clause([]):- !. output_kif_clause([OneLiteral]):- !, output_kif_signed_literal(OneLiteral). output_kif_clause([FirstLiteral|RestOfLiterals]):- output_kif_signed_literal(FirstLiteral), nl, write(' '), output_kif_clause(RestOfLiterals). %------------------------------------------------------------------------------ %----Output the clauses selected by status output_kif_clauses([]):- !. %----If the clause has an acceptable status then output output_kif_clauses([input_clause(Name,Role,Literals)|RestOfClauses]):- write('(cl:comment '), write('"'), write(Name), write(', '), write(Role), write('"'), nl, % write(' (or '), %----DANGER - CONSTANTS THAT LOOK LIKE VARIABLES GET TREATED AS VARIABLES fofify_literals(Literals,Disjunction), universally_quantify(Disjunction,QuantifiedDisjunction), output_generic_prefix_formula(kif,QuantifiedDisjunction), % output_kif_clause(Literals), % write(' ) )'), write(' )'), nl, nl, output_kif_clauses(RestOfClauses). %------------------------------------------------------------------------------ output_kif_clauses_by_roles(Clauses):- tptp2X_findall_setof1(Role,tptp2X_member(input_clause(_,Role,_),Clauses), Roles), tptp2X_member(Role,Roles), findall(input_clause(Name,Role,Clause),tptp2X_member(input_clause(Name, Role,Clause),Clauses),ClausesWithRole), write('(cl:text '), write(Role), nl, nl, output_kif_clauses(ClausesWithRole), write(')'), nl, nl, fail. output_kif_clauses_by_roles(_). %------------------------------------------------------------------------------ %----Output all the clauses in kif format kif(kif,Clauses,_):- tptp_clauses(Clauses), output_kif_clauses_by_roles(Clauses). %----Output all the formulae in kif format kif(kif,Formulae,_):- tptp_formulae(Formulae), output_kif_formulae_by_roles(Formulae). %------------------------------------------------------------------------------ %----Provide information about the kif format kif_format_information(';; ','.kif'). %------------------------------------------------------------------------------ %----Provide information about the kif file kif_file_information(format,kif,'KIF format'). %------------------------------------------------------------------------------