%=================================================================== %--- This transforms TPTP clauses and first order formulae into %--- bliksem format. %=================================================================== % Print the header for first order formulae: blk_fof_header :- nl, write( 'Auto.' ), nl, nl. % Print the header for CNF-clauses: blk_cnf_header :- nl, write('Set( totalproof, 1 ).'), nl, write('Set( prologoutput, 1 ).'), nl, write( 'Auto.' ), nl, nl. % True if all elements of L have form fof( Name, Type, F ). blk_isfof( [] ). blk_isfof( [ fof( _, _, _ ) | R ] ) :- blk_isfof( R ). % True if all elements of L have form input_clause( Name, Type, F ). blk_iscnf( [] ). blk_iscnf( [ input_clause( _, _, _ ) | R ] ) :- blk_iscnf( R ). blk_printvarlist( [] ) :- write( 'THIS SHOULD NOT HAPPEN' ). blk_printvarlist( [ F ] ) :- !, write( F ). blk_printvarlist( [ F | R ] ) :- write( F ), write( ', ' ), blk_printvarlist( R ). % Print a formula in fof format. We do not attempt make the result % human readable. blk_printfof( ~ A ) :- !, blk_printunary( '!', A ). % the final proof that Prolog cannot be trusted: blk_printfof( '|'(A,B) ) :- !, blk_printbinary( '|', A, B ). blk_printfof( (A ; B) ) :- !, blk_printbinary( '|', A, B ). blk_printfof( A & B ) :- !, blk_printbinary( '&', A, B ). blk_printfof( A <=> B ) :- !, blk_printbinary( '<->', A, B ). blk_printfof( A => B ) :- !, blk_printbinary( '->', A, B ). blk_printfof( A <= B ) :- !, blk_printbinary( '->', B, A ). blk_printfof( A <~> B ) :- !, blk_printnegbinary( '<->', A, B ). blk_printfof( A '~|' B ) :- !, blk_printnegbinary( '|', A, B ). blk_printfof( A ~& B ) :- !, blk_printnegbinary( '&', A, B ). blk_printfof( ! L : F ) :- !, blk_printquantifier( '[', ']', L, F ). blk_printfof( ? L : F ) :- !, blk_printquantifier( '<', '>', L, F ). blk_printfof( '$tptp_equal'( A, B ) ) :- !, blk_printbinary( '=', A, B ). blk_printfof('$true'):- !, write('( && )'). blk_printfof('$false'):- !, write('( || )'). blk_printfof( F ) :- write( F ). blk_printunary( _, A ) :- write( '! ( ' ), blk_printfof( A ), write( ')' ). blk_printbinary( Operator, A, B ) :- write( '(' ), blk_printfof( A ), write( ')' ), write( Operator ), write( '(' ), blk_printfof( B ), write( ')' ). blk_printnegbinary( Operator, A, B ) :- write( '! (( ' ), blk_printfof( A ), write( ')' ), write( Operator ), write( '(' ), blk_printfof( B ), write( '))' ). blk_printquantifier( Start, End, A, B ) :- write( '( ' ), write( Start ), blk_printvarlist( A ), write( End ), blk_printfof( B ), write( ')' ). % Print a list of first order formulae. A '.' is inserted after every % formula, together with a newline. blk_printfoflist( [] ). blk_printfoflist( [ fof( Name, Status, F ) | R ] ) :- tptp2X_member(Status,[axiom,hypothesis,lemma,definition]), !, write( '# '), write(Status), write(' ' ), write( Name ), write( ':' ), nl, !, blk_printfof( F ), !, write( '.' ), nl, blk_printfoflist( R ). blk_printfoflist( [ fof( Name, conjecture, F ) | R ] ) :- %----Need this for dodgy processing in Ratify write('#----This is the conjecture with negated conjecture'), nl, write( '# conjecture (has been negated) '), write( Name ), write( ':' ), nl, !, blk_printfof( ~ F ), !, write( '.' ), nl, blk_printfoflist( R ). % Print atoms: An atom can be printed without problems, because bliksem % has the Prolog convention for variables. '$tptp_equal'(A,B) has to be % replaced by A = B. blk_printatom( '$tptp_equal'( A, B ) ) :- write( A = B ), !. blk_printatom('$true'):- !, write(' && '). blk_printatom('$false'):- !, write(' || '). blk_printatom( X ) :- write( X ). % Print a literal: ++ X is printed as X. -- X is printed as ! X. blk_printliteral( ++ X ) :- blk_printatom( X ). blk_printliteral( -- X ) :- write( '! ' ), blk_printatom( X ). % Print list of literals, separated by comma's. blk_printliterals( [] ). blk_printliterals( [ F ] ) :- !, blk_printliteral( F ), write( ' ' ). blk_printliterals( [ F | R ] ) :- blk_printliteral( F ), write( ', ' ), blk_printliterals( R ). % Print a clause: blk_printclause( Cls ) :- write( '{ ' ), blk_printliterals( Cls ), write( '}.' ). % Print a clause list: blk_printclauselist( [] ). blk_printclauselist( [ input_clause( Name, Type, F ) | R ] ) :- write( '# ' ), write( Type ), write( ' ' ), write( Name ), write( ':' ), nl, !, blk_printclause( F ), !, nl, blk_printclauselist( R ). % Convert TPTP to bliksem. It is necessary to check the format in advance % in order to produce the right header. bliksem( bliksem, Formulalist, _ ) :- blk_isfof( Formulalist ), !, blk_fof_header, blk_printfoflist( Formulalist ), nl. bliksem( bliksem, Formulalist, _ ) :- blk_iscnf( Formulalist ), !, blk_cnf_header, blk_printclauselist( Formulalist ), nl. bliksem( bliksem, Formulalist, _ ) :- write( 'Sorry, cannot handle this: ' ), write( Formulalist ), nl. % We chose # for comment. % was not possible because it is allowed in % identifiers. bliksem_format_information( '#', '.blk' ). bliksem_file_information( format, bliksem, 'Bliksem format' ).