/*************************************************************************
File: callInference.pl
Copyright (C) 2004 Patrick Blackburn & Johan Bos
This file is part of BB1, version 1.2 (August 2005).
BB1 is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
BB1 is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with BB1; if not, write to the Free Software Foundation, Inc.,
59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
*************************************************************************/
:- module(callInference,[infix/0,
prefix/0,
callTP/3,
callMB/4,
callTPandMB/6,
mbTestSuite/0,
tpTestSuite/0,
tpmbTestSuite/0]).
:- use_module(fol2otter,[fol2otter/2,
fol2mace/2]).
:- use_module(fol2bliksem,[fol2bliksem/2]).
:- use_module(fol2tptp,[fol2tptp/2]).
:- use_module(comsemPredicates,[infix/0,
prefix/0,
appendLists/3,
memberList/2,
selectFromList/3,
executeCommand/1,
concatStrings/2]).
:- use_module(folTestSuite,[formula/2]).
:- [inferenceEngines].
/*========================================================================
Initialise Theorem Provers
========================================================================*/
initTheoremProvers([],_).
initTheoremProvers([otter|L],Formula):- !,
open('otter.in',write,Stream),
fol2otter(not(Formula),Stream),
close(Stream),
initTheoremProvers(L,Formula).
initTheoremProvers([bliksem|L],Formula):- !,
open('bliksem.in',write,Stream),
fol2bliksem(not(Formula),Stream),
close(Stream),
% executeCommand('dos2unix bliksem.in'), %%% use for MS-DOS/Windows
initTheoremProvers(L,Formula).
initTheoremProvers([_|L],Formula):-
initTheoremProvers(L,Formula).
/*========================================================================
Initialise Model Builders
========================================================================*/
initModelBuilders([],_).
initModelBuilders([mace|L],Formula):- !,
open('mace.in',write,Stream),
fol2mace(Formula,Stream),
close(Stream),
initModelBuilders(L,Formula).
initModelBuilders([paradox|L],Formula):- !,
open('paradox.in',write,Stream),
fol2tptp(not(Formula),Stream),
close(Stream),
initModelBuilders(L,Formula).
initModelBuilders([_|L],Formula):-
initModelBuilders(L,Formula).
/*========================================================================
Calls to Theorem Provers
========================================================================*/
callTP(Problem,Proof,Engine):-
executeCommand('chmod 700 interfaceTP.perl'),
inferenceEngines(Engines),
initTheoremProvers(Engines,Problem),
concatStrings(['perl ./interfaceTP.perl '|Engines],Shell),
executeCommand(Shell),
open('tp.out',read,Out),
read(Out,Result),
(
Result=proof, !,
read(Out,engine(Engine)),
Proof=proof
;
Proof=unknown,
Engine=unknown
),
close(Out).
/*========================================================================
Calls to Model Builders
========================================================================*/
callMB(Problem,DomainSize,Model,Engine):-
executeCommand('chmod 700 interfaceMB.perl'),
number(DomainSize),
inferenceEngines(Engines),
initModelBuilders(Engines,Problem),
concatStrings(['perl ./interfaceMB.perl ',DomainSize,' '|Engines],Shell),
executeCommand(Shell),
open('mb.out',read,Out),
read(Out,Result),
(
Result=interpretation(_,_),
read(Out,engine(Engine)),
mace2blackburnbos(Result,Model), !
;
Result=paradox(_),
read(Out,engine(Engine)),
paradox2blackburnbos(Result,Model), !
;
Model=unknown,
Engine=unknown
),
close(Out).
/*========================================================================
Calls to Theorem Provers and Model Builders
========================================================================*/
callTPandMB(TPProblem,MBProblem,DomainSize,Proof,Model,Engine):-
executeCommand('chmod 700 interfaceTPandMB.perl'),
number(DomainSize),
inferenceEngines(Engines),
initTheoremProvers(Engines,TPProblem),
initModelBuilders(Engines,MBProblem),
concatStrings(['perl ./interfaceTPandMB.perl ',DomainSize,' '|Engines],Shell),
executeCommand(Shell),
open('tpmb.out',read,Out),
read(Out,Result),
(
Result=proof, !,
read(Out,engine(Engine)),
Proof=proof,
Model=unknown
;
Result=interpretation(_,_),
read(Out,engine(Engine)),
mace2blackburnbos(Result,Model), !,
Proof=unknown
;
Result=paradox(_),
read(Out,engine(Engine)),
paradox2blackburnbos(Result,Model), !,
Proof=unknown
;
Model=unknown,
Proof=unknown,
Engine=unknown
),
close(Out).
/*========================================================================
Prove all formulas from the test suite (using Theorem Provers)
========================================================================*/
tpTestSuite:-
format('~n~n>>>>> INFERENCE TEST SUITE <<<<<',[]),
formula(Formula,Status),
format('~nInput formula: ~p~nStatus: ~p',[Formula,Status]),
callTP(Formula,Proof,Engine),
(
Proof=proof,
Result=theorem
;
\+ Proof=proof,
Result=unknown
),
format('~nInference engine ~p says: ~p~n',[Engine,Result]),
fail.
tpTestSuite.
/*========================================================================
Build models for formulas from the test suite (using Model Builders)
========================================================================*/
mbTestSuite:-
format('~n~n>>>>> INFERENCE TEST SUITE <<<<<',[]),
formula(Formula,Status),
format('~nInput formula: ~p~nStatus: ~p',[Formula,Status]),
callMB(Formula,30,Model,Engine),
format('~nInference engine ~p says: ~p~n',[Engine,Model]),
fail.
mbTestSuite.
/*========================================================================
Prove or build models for all formulas from the test suite
(using Theorem Provers and model builders)
========================================================================*/
tpmbTestSuite:-
format('~n~n>>>>> INFERENCE TEST SUITE <<<<<',[]),
formula(Formula,Status),
format('~nInput formula: ~p~nStatus: ~p',[Formula,Status]),
callTPandMB(Formula,Formula,30,Proof,Model,Engine),
(
Proof=proof,
Result=theorem
;
Proof=unknown,
Model=model(_,_),
Result=Model
;
Proof=unknown,
Model=unknown,
Result=unknown
),
format('~nInference engine ~p says: ~p~n',[Engine,Result]),
fail.
tpmbTestSuite.
/*========================================================================
Translate Paradox-type Model into Blackburn & Bos Models
========================================================================*/
paradox2blackburnbos(Paradox,model(D,F)):-
Paradox = paradox(Terms), \+ Terms=[],
paradox2d(Terms,[d1]-D),
paradox2f(Terms,[]-F).
paradox2blackburnbos(Paradox,model([],[])):-
Paradox = paradox([]).
paradox2blackburnbos(Paradox,unknown):-
\+ Paradox = paradox(_).
/*========================================================================
Translate Paradox Terms to Domain
========================================================================*/
paradox2d([],D-D).
paradox2d([_Constant=Entity|L],D1-D2):-
\+ memberList(Entity,D1), !,
paradox2d(L,[Entity|D1]-D2).
paradox2d([Symbol:1|L],D1-D2):-
functor(Symbol,_Functor,1),
arg(1,Symbol,Entity),
\+ memberList(Entity,D1), !,
paradox2d(L,[Entity|D1]-D2).
paradox2d([Symbol:1|L],D1-D2):-
functor(Symbol,_Functor,2),
arg(1,Symbol,Entity1),
arg(2,Symbol,Entity2),
(
\+ memberList(Entity1,D1), !,
(
\+ memberList(Entity2,D2), !,
paradox2d(L,[Entity1,Entity2|D1]-D2)
;
paradox2d(L,[Entity1|D1]-D2)
)
;
\+ memberList(Entity2,D2),
paradox2d(L,[Entity2|D1]-D2)
), !.
paradox2d([_|L],D1-D2):-
paradox2d(L,D1-D2).
/*========================================================================
Translate Paradox Terms to Interpretation Function
========================================================================*/
paradox2f([],F-F).
paradox2f([Constant=Entity|L],D1-D2):-
Term = f(0,Constant,Entity),
\+ memberList(Term,D1), !,
paradox2f(L,[Term|D1]-D2).
paradox2f([Symbol:1|L],D1-D2):-
functor(Symbol,Functor,1), !,
arg(1,Symbol,Arg),
(
selectFromList(f(1,Functor,E),D1,D3), !,
paradox2f(L,[f(1,Functor,[Arg|E])|D3]-D2)
;
paradox2f(L,[f(1,Functor,[Arg])|D1]-D2)
).
paradox2f([Symbol:0|L],D1-D2):-
functor(Symbol,Functor,1), !,
(
memberList(f(1,Functor,_),D1), !,
paradox2f(L,D1-D2)
;
paradox2f(L,[f(1,Functor,[])|D1]-D2)
).
paradox2f([Symbol:1|L],D1-D2):-
functor(Symbol,Functor,2), !,
arg(1,Symbol,Arg1),
arg(2,Symbol,Arg2),
(
selectFromList(f(2,Functor,E),D1,D3), !,
paradox2f(L,[f(2,Functor,[(Arg1,Arg2)|E])|D3]-D2)
;
paradox2f(L,[f(2,Functor,[(Arg1,Arg2)])|D1]-D2)
).
paradox2f([Symbol:0|L],D1-D2):-
functor(Symbol,Functor,2), !,
(
memberList(f(2,Functor,_),D1), !,
paradox2f(L,D1-D2)
;
paradox2f(L,[f(2,Functor,[])|D1]-D2)
).
paradox2f([_|L],D1-D2):-
paradox2f(L,D1-D2).
/*========================================================================
Translate Mace-type Model into Blackburn & Bos Models
========================================================================*/
mace2blackburnbos(Mace,model(D,F)):-
Mace = interpretation(Size,Terms),
mace2d(1,Size,D),
mace2f(Terms,D,F).
mace2blackburnbos(Mace,unknown):-
\+ Mace = interpretation(_Size,_Terms).
/*========================================================================
Translate Mace Model to Domain
========================================================================*/
mace2d(N,N,[V]):-
name(N,Codes),
name(V,[100|Codes]).
mace2d(I,N,[V|D]):-
I < N,
name(I,Codes),
name(V,[100|Codes]),
J is I + 1,
mace2d(J,N,D).
/*========================================================================
Translate Mace Model to Interpretation Function
========================================================================*/
mace2f([],_,[]):- !.
mace2f([function(Skolem,_)|Terms],D,F):-
\+ atom(Skolem), !,
mace2f(Terms,D,F).
mace2f([function(Constant,[V])|Terms],D,[f(0,Constant,X)|F]):-
atom(Constant), !,
Index is V + 1,
name(Index,Codes),
name(X,[100|Codes]),
mace2f(Terms,D,F).
mace2f([predicate(Relation,V)|Terms],D,[f(1,Functor,X)|F]):-
Relation =.. [Functor,_], !,
positiveValues(V,1,X),
mace2f(Terms,D,F).
mace2f([predicate(Relation,V)|Terms],D,[f(2,Functor,X)|F]):-
Relation =.. [Functor,_,_], !,
length(D,Size),
positivePairValues(V,Size,1,1,X),
mace2f(Terms,D,F).
mace2f([_|Terms],D,F):-
mace2f(Terms,D,F).
/*========================================================================
Take positive values of one-place predicates
========================================================================*/
positiveValues([],_,[]).
positiveValues([1|Values],I1,[X|Rest]):-
name(I1,Codes),
name(X,[100|Codes]),
I2 is I1 + 1,
positiveValues(Values,I2,Rest).
positiveValues([0|Values],I1,Rest):-
I2 is I1 + 1,
positiveValues(Values,I2,Rest).
/*========================================================================
Take positive values of two-place predicates
========================================================================*/
positivePairValues([],_,_,_,[]).
positivePairValues([1|Values],Size,I1,J1,[(X2,X1)|Rest]):-
name(I1,Codes1),
name(X1,[100|Codes1]),
name(J1,Codes2),
name(X2,[100|Codes2]),
(
I1 < Size,
I2 is I1 + 1,
J2 is J1
;
I1 = Size,
I2 = 1,
J2 is J1 + 1
),
positivePairValues(Values,Size,I2,J2,Rest).
positivePairValues([0|Values],Size,I1,J1,Rest):-
(
I1 < Size,
I2 is I1 + 1,
J2 is J1
;
I1 = Size,
I2 = 1,
J2 is J1 + 1
),
positivePairValues(Values,Size,I2,J2,Rest).
/*========================================================================
Info
========================================================================*/
info:-
inferenceEngines(Engines),
format('~n> ---------------------------------------------------------- <',[]),
format('~n> callInference.pl, by Patrick Blackburn and Johan Bos <',[]),
format('~n> <',[]),
format('~n> ?- callTP(Problem,Proof,Engine). <',[]),
format('~n> ?- callMB(Problem,DomainSize,Model,Engine) <',[]),
format('~n> ?- callTPandMB(TPProblem,MBProblem,Size,Proof,Model,Eng). <',[]),
format('~n> ?- mbTestSuite. <',[]),
format('~n> ?- tpTestSuite. <',[]),
format('~n> ?- tpmbTestSuite. <',[]),
format('~n> ?- infix. <',[]),
format('~n> ?- prefix. <',[]),
format('~n> <',[]),
format('~n> Selected Inference Engines (inferenceEngines/1) <',[]),
format('~n> ~p',[Engines]),
format('~n> ---------------------------------------------------------- <',[]),
format('~n~n',[]).
/*========================================================================
Display info at start
========================================================================*/
:- info.