%======================================================================== %----This outputs TPTP Problem Set clauses in a format acceptable to %----the leanCoP system. %---- %----Written by Jens Otten, March 2000 %----Based on format.leantap %======================================================================== %----Print out a literal with - for negative, nothing for positive. %----Use positive representation 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([]):- !. output_leancop_clauses([input_clause(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). %---------------------------------------------------------------------- %----Print out 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 all the clauses in leanCoP format. leancop(leancop,Clauses,_):- tptp_clauses(Clauses), output_leancop_formula(Clauses). %----Do nothing for FOF - just leave a comment leancop(leancop,Formulae,_):- tptp_formulae(Formulae), write('%----No FOF format available in leanCoP'), nl. %---------------------------------------------------------------------- %----Provide information about the leanCoP format. leancop_format_information('%','.leancop'). %---------------------------------------------------------------------- %----Provide information about the TPTP file leancop_file_information(format,leancop). %----------------------------------------------------------------------