%============================================================================== %----Procedures for writing out formulae in MetiTarski format %---- %----Written by Geoff Sutcliffe, February 2010 %============================================================================== %----Generic output %============================================================================== %------------------------------------------------------------------------------ tptp_to_metitarski(TPTPBinary,Arity,MetiTarskiInfix):- tptp2X_member(TPTPBinary/Arity-MetiTarskiInfix,[ %----These are in the TPTP language '$less'/2-'<', '$lesseq'/2-'<=', '$greater'/2-'>', '$greatereq'/2-'>=', '$sum'/2-'+', '$difference'/2-'-', '$product'/2-'*', '$uminus'/1-'-', %----These are available in MetiTarski '$pi'/0-pi, '$quotient'/2-'/', '$abs'/1-abs, '$pow'/2-'^', '$sqrt'/1-sqrt, '$exp'/1-exp, '$ln'/1-ln, '$sin'/1-sin, '$cos'/1-cos, '$tan'/1-tan, '$arctan'/1-arctan, '$sinh'/1-sinh, '$cosh'/1-cosh, '$tanh'/1-tanh ]). %------------------------------------------------------------------------------ %----Output variables metitarski_output_variable(_Langauge,Variable):- tptp_output_variable(Variable). metitarski_output_variable(Variable):- tptp_output_variable(Variable). %------------------------------------------------------------------------------ metitarski_output_atom_list(Langauge,[One]):- !, metitarski_output_atom(Langauge,One). metitarski_output_atom_list(Langauge,[One,Two|Rest]):- metitarski_output_atom(Langauge,One), write(','), metitarski_output_atom_list(Langauge,[Two|Rest]). %------------------------------------------------------------------------------ metitarski_output_atom(Language,Variable):- looks_like_a_variable(Variable), !, metitarski_output_variable(Language,Variable). metitarski_output_atom(_Language,Atom):- atomic(Atom), tptp_to_metitarski(Atom,0,MetiTarskiAtom), !, write('('), write(' '),write(MetiTarskiAtom),write(' '), write(')'). metitarski_output_atom(_Language,Atom):- atomic(Atom), !, write(Atom). %----Rational terms metitarski_output_atom(Language,Numerator/Denominator):- metitarski_output_atom(Language,Numerator), write('/'), metitarski_output_atom(Language,Denominator). metitarski_output_atom(Language,'$tptp_equal'(X,Y)):- !, metitarski_output_atom(Language,X), write(' = '), metitarski_output_atom(Language,Y). metitarski_output_atom(Language,X = Y):- !, metitarski_output_atom(Language,X), write(' = '), metitarski_output_atom(Language,Y). metitarski_output_atom(Language,'$tptp_not_equal'(X,Y)):- !, metitarski_output_atom(Language,X), write(' != '), metitarski_output_atom(Language,Y). metitarski_output_atom(Language,X != Y):- !, metitarski_output_atom(Language,X), write(' != '), metitarski_output_atom(Language,Y). metitarski_output_atom(Language,Term):- Term =.. [TPTPUnary,Operand], tptp_to_metitarski(TPTPUnary,1,MetiTarskiPrefix), !, write(' '),write(MetiTarskiPrefix),write('('), metitarski_output_atom(Language,Operand), write(')'). metitarski_output_atom(Language,Term):- Term =.. [TPTPBinary,LHS,RHS], tptp_to_metitarski(TPTPBinary,2,MetiTarskiInfix), !, write('('), metitarski_output_atom(Language,LHS), write(' '),write(MetiTarskiInfix),write(' '), metitarski_output_atom(Language,RHS), write(')'). metitarski_output_atom(Language,Term):- Term =.. [Functor|Arguments], write(Functor), write('('), metitarski_output_atom_list(Language,Arguments), write(')'). %------------------------------------------------------------------------------ %============================================================================== %----FOF format %============================================================================== %------------------------------------------------------------------------------ metitarski_quantified_formula(QuantifiedFormula,Quantifier,Variables,Formula):- tptp_quantified_formula(QuantifiedFormula,Quantifier,Variables,Formula). metitarski_binary_formula(BinaryFormula,BinaryConnective,LHS,RHS):- tptp_binary_formula(BinaryFormula,BinaryConnective,LHS,RHS). metitarski_unary_formula(UnaryFormula,UnaryConnective,Formula):- tptp_unary_formula(UnaryFormula,UnaryConnective,Formula). %------------------------------------------------------------------------------ %----The format for outputing quantified formulae in MetiTarski format %----FormulaPrefix,VariablesPrefix,VariablesSeparator,VariablesSuffix, %----FormulaSuffix metitarski_quantified_format(FormulaPrefix,VariablesPrefix,VariablesSeparator, VariablesSuffix,FormulaSuffix):- tptp_quantified_format(FormulaPrefix,VariablesPrefix,VariablesSeparator, VariablesSuffix,FormulaSuffix). %----FormulaPrefix,ConnectivePrefix,ConnectiveSuffix,FormulaSuffix metitarski_binary_format(FormulaPrefix,ConnectivePrefix,ConnectiveSuffix, FormulaSuffix):- tptp_binary_format(FormulaPrefix,ConnectivePrefix,ConnectiveSuffix, FormulaSuffix). %----FormulaPrefix,ConnectiveSuffix,FormulaSuffix metitarski_unary_format(FormulaPrefix,ConnectiveSuffix,FormulaSuffix):- tptp_unary_format(FormulaPrefix,ConnectiveSuffix,FormulaSuffix). %------------------------------------------------------------------------------ metitarski(metitarski,Formulae,_):- tptp_formulae(Formulae), !, convert_formulae_to_tptp(Formulae,TSTPFormulae), output_tptp_formulae(metitarski,short,TSTPFormulae). metitarski(metitarski,_,_):- !, write('%----ERROR: No MetiTarski format for that type of file'), nl. %------------------------------------------------------------------------------ %----Provide information about the MetiTarski format metitarski_format_information('%','.mski'). %------------------------------------------------------------------------------ %----Provide information about the TSTP file metitarski_file_information(format,metitarski,'MetiTarski'). %------------------------------------------------------------------------------