/* Realization constructor for propositional K4 into J4. It is a combination
of a quasi-realization program for K4 and a quasi-realization to
realization program. It begins by constructing a (destructive) tableau
proof. Then it fills that out, from branch end up, to make a mixed
tableau, from which a quasi-realization is extracted. Then this is
converted into a realization. Information is displayed for both
quasi-realizations and realizations.
The tableau construction uses signed formulas. These are implemented
simply as f(X) and t(X). When a pi rule is applied, a counter is
decremented. This is the simplest way of avoiding infinite regress
(looping).
Propositional operators are: neg, and, or, imp.
The binary connectives are right associative. Box is the only modal
operator. There is also a dedicated constant, bot (falsehood).
In addition there is ::, for the "justifies" predicate (: was already
in use). It is right associative. And there is * for the dot,
or application, operator, and + as usual. Both are left associative.
Parentheses are recommended.
When reading output, justification variables are v1, v2, etc.
Justification terms, introduced at the quasi-realization stage,
are j1, j2, etc. Those introduced at the realization stage
are t1, t2, etc.
The implementation uses the swipl library, specifically for its
member, union, and subtract predicates.
May, 2014
Melvin Fitting
*/
/*********************************************************************/
/* SYNTAX */
:-op(140, fy, [neg, box]).
:-op(160, xfy, [and, or, imp, ::]).
:-op(160, yfx, [*]).
/*
Uniform notation for propositional connectives is used.
Since only box is permitted as a modal operator, modal
uniform notation is not used.
*/
/* conjunctive(X) :- X is a signed alpha formula.
*/
conjunctive(t(_ and _)).
conjunctive(f(_ or _)).
conjunctive(f(_ imp _)).
/* disjunctive(X) :- X is a signed beta formula.
*/
disjunctive(f(_ and _)).
disjunctive(t(_ or _)).
disjunctive(t(_ imp _)).
/* unary(X) :- X is a signed negation.
*/
unary(f(neg _)).
unary(t(neg _)).
/* components(X, Y, Z) :- Y and Z are the components
of the signed formula X, as defined in the alpha
and beta tables.
*/
components(t(X and Y), t(X), t(Y)).
components(f(X and Y), f(X), f(Y)).
components(t(X or Y), t(X), t(Y)).
components(f(X or Y), f(X), f(Y)).
components(t(X imp Y), f(X), t(Y)).
components(f(X imp Y), t(X), f(Y)).
/* component(X, Y) :- Y is the component of the
unary formula X.
*/
component(f(neg X), t(X)).
component(t(neg X), f(X)).
/* propAtom(X) :- X is a signed propositional letter.
*/
propAtom(t(X)) :- atom(X).
propAtom(f(X)) :- atom(X).
/* Justification variables will be v1, v2, etc, and justification
terms will be j1, j2, etc, and t1, t2, etc. These are generated
using gensym. The following resets the counters. Also, what each
justification term serves to justify is recorded using
assert, so that a table of values can be displayed at the end.
The reset instruction also erases earlier results.
*/
reset :-
reset_gensym(v),
reset_gensym(j),
reset_gensym(t),
retractall(proves(_, _)),
retractall(where(_,_,_,_,_)).
/* Formulas must be annotated, with indexed occurrences of box.
Eventually positive occurrences of indexed boxes must be replaced
with justification variables. It is simplest to just replace
all box occurrences with justification variables up front, and treat
them as if they were indexed boxes during the tableau construction.
This avoids some complexity later on. So, in the tableau
construction below, box P will actually appear as vn::P, where
vn is a justification variable.
annotate(X, Y) :- X is a signed formula and Y is the result
of replacing each occurrence of box in X with an occurrence
of a new justification variable vn, so that Y is a signed
formula of justification logic.
*/
annotate(X, X) :-
propAtom(X).
annotate(Binary, NewBinary) :-
conjunctive(Binary),
components(Binary, Binaryone, Binarytwo),
annotate(Binaryone, NewBinaryone),
annotate(Binarytwo, NewBinarytwo),
conjunctive(NewBinary),
components(NewBinary, NewBinaryone, NewBinarytwo).
annotate(Binary, NewBinary) :-
disjunctive(Binary),
components(Binary, BinaryOne, BinaryTwo),
annotate(BinaryOne, NewBinaryOne),
annotate(BinaryTwo, NewBinaryTwo),
disjunctive(NewBinary),
components(NewBinary, NewBinaryOne, NewBinaryTwo).
annotate(Negation, NewNegation) :-
unary(Negation),
component(Negation, Body),
annotate(Body, NewBody),
component(NewNegation, NewBody).
annotate(t(box Body), t(Var :: NewBody)) :-
annotate(t(Body), t(NewBody)),
gensym(v, Var).
annotate(f(box Body), f(Var :: NewBody)) :-
annotate(f(Body), f(NewBody)),
gensym(v, Var).
/***************************************************************/
/* TABLEAU CONSTRUCTION */
/* closes(MixedTableau, D) :- MixedTableau can be expanded to one whose
modal part is closed, using modal depth D, a limit on the number of
pi rule applications. Then the justification part is filled in,
branch end to root, to produce a proper closed mixed tableau. If
closure is not possible, a call fails.
A mixed tableau is a list of its branches. A branch is a list
of the items on it. Each item is of the form mixed(A, B), where
A is a signed modal formula and B is a list of signed justification
formulas. Although lists are used to represent branches,
they are treated as sets, and all repetitions are removed.
Closure is always atomic closure. Then the trivial(Branch) operation
in the atomic closure clauses below provides justification counterparts
for all formulas on the branch, including the one or ones that caused
the branch to close. Here we make use of the fact that,
even in modal formulas, indexed box operators have been represented
by justification variables.
The order of these clauses is important. If a tableau proof can be
found, any ordering will serve, but some will find more complex proofs
than others, with useless steps. This will be reflected in the
complexity of the quasi-realizers.
*/
/* ATOMIC */
closes([Branch | Rest], D) :-
member(mixed(t(bot), _), Branch),
trivial(Branch),
closes(Rest, D).
closes([Branch | Rest], D) :-
member(mixed(t(X), _), Branch),
member(mixed(f(X), _), Branch),
propAtom(t(X)),
trivial(Branch),
closes(Rest, D).
/* UNARY RULE */
closes([Branch | Rest], D) :-
member(mixed(Negation, JNegatedList), Branch),
unary(Negation),
component(Negation, UnNegated),
subtract(Branch, [mixed(Negation, JNegatedList)], Temporary),
union([mixed(UnNegated, JUnNegatedList)], Temporary, NewBranch),
closes([NewBranch | Rest], D),
negate(JUnNegatedList, JNegatedList).
/* ALPHA RULE */
closes([Branch | Rest], D) :-
member(mixed(Alpha, JAlphaList), Branch),
conjunctive(Alpha),
components(Alpha, AlphaOne, AlphaTwo),
subtract(Branch, [mixed(Alpha, JAlphaList)], Temporary),
union([mixed(AlphaOne, JAlphaOneList),
mixed(AlphaTwo, JAlphaTwoList)], Temporary, NewBranch),
closes([NewBranch | Rest], D),
combineJLists(Alpha, JAlphaOneList, JAlphaTwoList, JAlphaList).
/* BETA RULE */
closes([Branch | Rest], D) :-
member(mixed(Beta,JBetaList), Branch),
disjunctive(Beta),
components(Beta, BetaOne, BetaTwo),
subtract(Branch, [mixed(Beta, JBetaList)], Temporary),
copy_term(Temporary, TempBranchOne),
copy_term(Temporary, TempBranchTwo),
union([mixed(BetaOne, _)], TempBranchOne, NewBranchOne),
union([mixed(BetaTwo, _)], TempBranchTwo, NewBranchTwo),
closes([NewBranchOne | Rest], D),
closes([NewBranchTwo | Rest], D),
combineBranches(TempBranchOne, TempBranchTwo, Temporary),
member(mixed(BetaOne, JBetaOneList), NewBranchOne),
member(mixed(BetaTwo, JBetaTwoList), NewBranchTwo),
combineJLists(Beta, JBetaOneList, JBetaTwoList, JBetaList).
/* PI RULE */
closes([Branch | Rest], D) :-
member(mixed(f(Var :: Fmla), [f(Term :: Disjunction)]), Branch),
D > 1,
subtract(Branch, [mixed(f(Var :: Fmla), [f(Term :: Disjunction)])],
ReducedBranch), sharp(ReducedBranch, Temporary),
union([mixed(f(Fmla), JList)], Temporary, NewBranch),
NewD is D - 1,
closes([NewBranch | Rest], NewD),
disjunctionOfList(JList, Disjunction),
trivial(ReducedBranch),
gensym(j, Term),
assert(proves(Term, NewBranch)).
closes([], _D).
/****************************************************************/
/* UTILITIES FOR TABLEAU CONSTRUCTION */
/* The pi-rule in the tableau construction modifies an entire
branch, using the so-called sharp operation. Since mixed
tableaus are now in use, sharp must take that into account.
sharp(A, B) :- the S4 sharp operation applied to tableau branch A
produces branch B. This is designed to be applied to a
mixed tableau, with the justification portion essentially
ignored. The S4 operation is not the same as the one for K.
Also note that during application, occurrences of u(X) are
changed back to t(X).
*/
sharp(X, Y) :- sharp_(X, Y), !.
sharp_([], []).
sharp_([mixed(t(V :: F), _) | Tail],
[mixed(t(V :: F), _), mixed(t(F), _) | NewTail]) :-
sharp_(Tail, NewTail).
sharp_([_Head|Tail], New) :-
sharp_(Tail, New).
/* trivial(List) :- Prolog variables are bound in List
so that the result is a mixed tableau branch displaying
a quasi-realization.
*/
trivial([mixed(_, Y) | Rest]) :- ground(Y), trivial(Rest).
trivial([mixed(t(X), [t(X)]) | Rest]) :- trivial(Rest).
trivial([mixed(f(X), [f(X)]) | Rest]) :- trivial(Rest).
trivial([mixed(u(X), [t(X)]) | Rest]) :- trivial(Rest).
trivial([]).
/* negate(List, NegatedList) :-
List is a list of signed formulas, and NegatedList is the result of
negating each member. That is, t(X) becomes t(neg X), and so on.
*/
negate([F | Rest], [G | NewRest]) :-
unary(G),
component(G, F),
negate(Rest, NewRest).
negate([], []).
/* combineBranches(InOne, InTwo, Out) :-
Initially InOne, InTwo, and Out are lists (sets) that contain
entries of the form mixed(Formula, JustificationList), with Formula
instantiated in all three lists, but JustificationList
instantiated in just the lists InOne and InTwo. After execution,
JustificationList in mixed(Formula, JustificationList),
in the list Out is instantiated to be the union of the corresponding
JustificationList parameters in InOne and InTwo, involving the
same Formula.
*/
combineBranches([mixed(Formula, ListOne) | Rest], InTwo, Out) :-
member(mixed(Formula, ListTwo), InTwo),
union(ListOne, ListTwo, ListOut),
member(mixed(Formula, ListOut), Out),
combineBranches(Rest, InTwo, Out).
combineBranches([], _, _).
/* combineJLists(Formula, List1, List2, CombinedList) :-
List1 is a list of signed formulas having the same sign,
List2 is a list of signed formulas having the same sign,
CombinedList is the result of combining each member of List1
with each member of List 2 to produce a formula of the same
type as Formula, with the original members as components.
*/
combineJLists(Formula, [H|T], List2, CombinedList) :-
combineSingle(Formula, H, List2, One),
combineJLists(Formula, T, List2, Two),
union(One, Two, CombinedList).
combineJLists(_, [], _, []).
/* combineSingle(Formula, Comp1, List, NewList) :-
NewList is the result of replacing each member Comp2
of List with BinaryFormula, where
constructBinary(Formula, Comp1, Comp2, BinaryFormula).
*/
combineSingle(Formula, Comp1, [H|T], NewList) :-
combineSingle(Formula, Comp1, T, One),
constructBinary(Formula, Comp1, H, Two),
union(One, [Two], NewList).
combineSingle(_, _, [], []).
/* constructBinary(Formula, Comp1, Comp2, BinaryFormula) :-
all four variables are signed formulas, and BinaryFormula
is constructed so that it has Comp1 and Comp2 as its
components, and is of the same type as Formula---that is,
both Formula and BinaryFormula are alpha or both are beta.
*/
constructBinary(Formula, AlphaOne, AlphaTwo, Alpha) :-
conjunctive(Formula),
conjunctive(Alpha),
components(Alpha, AlphaOne, AlphaTwo).
constructBinary(Formula, BetaOne, BetaTwo, Beta) :-
disjunctive(Formula),
disjunctive(Beta),
components(Beta, BetaOne, BetaTwo).
/* deSharp(Var, List, NewList) :-
Var is a justification variable. List is a list of justification
formulas having sign t. NewList is the result of replacing each
member t(X) in List with t(Var :: X).
*/
deSharp(_, [],[]).
deSharp(Var, [t(X) | T], [t(Var :: X) | NewT]) :-
deSharp(Var, T, NewT).
/* disjunctionOfList(List, Disj) :-
List consists of f-signed formulas, and Disj is
the disjunction of these formulas. This is used
in the pi-rule. Disjunction association is to the right.
*/
disjunctionOfList([f(A)], A).
disjunctionOfList([f(Head) | Tail], Head or X) :-
disjunctionOfList(Tail, X).
/**********************************************************************/
/* BUILDING MIXED TABLEAUS AND DISPLAYING OUTPUT */
/* test(X, D, PassOn) :-
X is a modal formula and D is a non-negative number, representing
modal depth. X is annotated and a mixed tableau for the
result, with an f sign, is constructed, using depth D. If it
succeeds in closing, success is anounced, the list of quasi-realizers
is displayed, and values for the justification terms are shown. PassOn
instantiates to the list of quasi-realizers, so it can be passed on to the
quasi-realizer to realizer conversion part.
*/
test(X, D, PassOn) :-
reset,
annotate(f(X), Y),
closes([[mixed(Y, Q)]], D),
nl, write('Propositional K4 tableau theorem'), nl, nl,
write('Quasi-realizing list consists of:'), nl, nl,
writeList(Q), nl,
removeF(Q, PassOn), /*this has been added*/
write('where:'), nl, nl,
writeQuasiReasons, nl.
writeList([f(Head) | Tail]) :- write(Head), nl, writeList(Tail).
writeList([]).
writeQuasiReasons :-
proves(X, Y),
getPremises(Y, Premises),
getConclusions(Y, Conclusions),
write(Premises), write(' -> '), write(X :: Conclusions), nl, fail.
writeQuasiReasons.
/* getPremises(List, Premises) :-
List is a branch of a mixed tableau.
is the list of formulas of the form
a :: b where t(a :: b) is on the
justification list of a member of List.
*/
getPremises(List, Premises) :-
getPremises_(List, Temp),
removeT(Temp, Premises), !.
getPremises_([mixed(t(_ :: _), L) | Rest], Premises) :-
getPremises_(Rest, Temp),
union(Temp, L, Premises).
getPremises_([_ | Rest], Premises) :-
getPremises_(Rest, Premises).
getPremises_([], []).
/* removeT(List, NewList) :-
List is a list of t-signed formulas and NewList is the
result of stripping off the signs.
*/
removeT([t(X) | Rest], [X | NewRest]) :-
removeT(Rest, NewRest).
removeT([], []).
/* getConclusions(List, Conclusions) :-
List is a branch of a mixed tableau. Conclusions
is the list of formulas f(F) where f(F) is on the
justification list of a member of List.
*/
getConclusions(List, Conclusions) :-
getConclusions_(List, Temp),
removeF(Temp, Conclusions), !.
getConclusions_([mixed(f(_), L) | Rest], Conclusions) :-
getConclusions_(Rest, Temp),
union(Temp, L, Conclusions).
getConclusions_([_ | Rest], Conclusions) :-
getConclusions_(Rest, Conclusions).
getConclusions_([], []).
/* removeF(List, NewList) :-
List is a list of f-signed formulas and NewList is the
result of stripping off the signs.
*/
removeF([f(X) | Rest], [X | NewRest]) :-
removeF(Rest, NewRest).
removeF([], []).
/**********************************************************/
/* NEXT THE CONVERSION FROM QUASI TO PROPER REALIZATION */
/**********************************************************/
/* THE CONVERSION PROCESS */
/* condense(QuasiSet, Signed, Realizer, Subst) :-
Signed
QuasiSet --------> (Realizer, Subst)
My notation is used above. It represents the following.
Signed is a signed modal formula. QuasiSet is a set of
quasi-realizers for Signed, and Realizer is a single
realizer for it. Subst is a substitution, represented as a
list of items, s(Var, Term), where Var is a variable and
Term is a term. If Signed has an f sign, the conjunction
of QuasiSet, with Subst applied, should imply Realizer.
If Signed has a t sign, Realizer should imply the
disjunction of QuasiSet, with Subst applied. This is
what the algorithm guarantees. The code below implements
the steps of the algorithm, but does not verify that
the implications hold. QuasiSet and Signed are inputs,
Realizer and Subst are outputs. The propositional steps below
are quite uniform, and could have been combined.
*/
/*Atomic case*/
condense([P], t(P), P, []) :- atom( P).
condense([P], f(P), P, []) :- atom(P).
/*T imp case*/
condense(QuasiSet, t(A imp B), Realizer, Subst) :-
separateBinary(QuasiSet, QuasiA, QuasiB),
condense(QuasiA, f(A), RealizerA, SubstA),
condense(QuasiB, t(B), RealizerB, SubstB),
sub(SubstB, RealizerA, Aprime),
sub(SubstA, RealizerB, Bprime),
Realizer = Aprime imp Bprime,
union(SubstA, SubstB, Subst).
/*F imp case*/
condense(QuasiSet, f(A imp B), Realizer, Subst) :-
separateBinary(QuasiSet, QuasiA, QuasiB),
condense(QuasiA, t(A), RealizerA, SubstA),
condense(QuasiB, f(B), RealizerB, SubstB),
sub(SubstB, RealizerA, Aprime),
sub(SubstA, RealizerB, Bprime),
Realizer = Aprime imp Bprime,
union(SubstA, SubstB, Subst).
/*T and case*/
condense(QuasiSet, t(A and B), Realizer, Subst) :-
separateBinary(QuasiSet, QuasiA, QuasiB),
condense(QuasiA, t(A), RealizerA, SubstA),
condense(QuasiB, t(B), RealizerB, SubstB),
sub(SubstB, RealizerA, Aprime),
sub(SubstA, RealizerB, Bprime),
Realizer = Aprime and Bprime,
union(SubstA, SubstB, Subst).
/*F and case*/
condense(QuasiSet, f(A and B), Realizer, Subst) :-
separateBinary(QuasiSet, QuasiA, QuasiB),
condense(QuasiA, f(A), RealizerA, SubstA),
condense(QuasiB, f(B), RealizerB, SubstB),
sub(SubstB, RealizerA, Aprime),
sub(SubstA, RealizerB, Bprime),
Realizer = Aprime and Bprime,
union(SubstA, SubstB, Subst).
/*T or case*/
condense(QuasiSet, t(A or B), Realizer, Subst) :-
separateBinary(QuasiSet, QuasiA, QuasiB),
condense(QuasiA, t(A), RealizerA, SubstA),
condense(QuasiB, t(B), RealizerB, SubstB),
sub(SubstB, RealizerA, Aprime),
sub(SubstA, RealizerB, Bprime),
Realizer = Aprime or Bprime,
union(SubstA, SubstB, Subst).
/*F or case*/
condense(QuasiSet, f(A or B), Realizer, Subst) :-
separateBinary(QuasiSet, QuasiA, QuasiB),
condense(QuasiA, f(A), RealizerA, SubstA),
condense(QuasiB, f(B), RealizerB, SubstB),
sub(SubstB, RealizerA, Aprime),
sub(SubstA, RealizerB, Bprime),
Realizer = Aprime or Bprime,
union(SubstA, SubstB, Subst).
/*T neg case*/
condense(QuasiSet, t(neg A), Realizer, Subst) :-
separateNeg(QuasiSet, QuasiA),
condense(QuasiA, f(A), Aprime, SubstA),
Realizer = neg Aprime,
Subst = SubstA.
/*F neg case*/
condense(QuasiSet, f(neg A), Realizer, Subst) :-
separateNeg(QuasiSet, QuasiA),
condense(QuasiA, t(A), Aprime, SubstA),
Realizer = neg Aprime,
Subst = SubstA.
/*T box case*/
condense(QuasiSet, t(box A), Realizer, Subst) :-
separateBox(QuasiSet, QuasiA),
condense(QuasiA, t(A), Aprime, SubstA),
tBoxProcess(QuasiA, Aprime, SubstA, S),
member(Var::_, QuasiSet),
Sigma = [s(Var, S * Var)],
sub(Sigma, Aprime, NewAprime),
Realizer = Var::NewAprime,
union(SubstA, Sigma, Subst).
/*F box case*/
condense(QuasiSet, f(box A), Realizer, Subst) :-
combineBoxDisj(QuasiSet, QuasiA, f(A)),
condense(QuasiA, f(A), Aprime, SubstA),
fBoxProcess(QuasiSet, Aprime, SubstA, T),
sub(SubstA, T::nothing, NewT::nothing),
Realizer = NewT::Aprime,
Subst = SubstA.
/********************************************************/
/* SUBSTITUTION */
/* sub(SubList, Formula, NewFormula) :-
SubList is a list of members of the form s(Var, Term),
where Var is a variable and Term is a justification term.
Formula is a justification logic formula.
NewFormula is the result of replacing all occurrences
of Var in Formula with occurrences of Term, for every
s(Var, Term) in SubList. Important note: It is assumed
that there is no "interference" between variables. That
is, replacing v by t does not introduce any variable that
will, themselves, need replacing. The "no new variable"
condition in the algorithm guarantees this. It greatly
simplifies the programming.
*/
sub([], Formula, Formula).
sub([s(Var, Term) | Rest], Formula, NewFormula) :-
subInFormula(Var, Formula, Term, Temp),
sub(Rest, Temp, NewFormula).
/* subInFormula(Var, Formula, Repl, NewFormula) :-
the result of replacing all occurrences of variable Var
in formula Formula with occurrences of Repl
is NewFormula. Does not check that Var is a variable.
*/
subInFormula(_Var, PropLetter, _Repl, PropLetter) :-
atom(PropLetter).
subInFormula(Var, J :: A, Repl, NewJ :: NewA) :-
subInTerm(Var, J, Repl, NewJ),
subInFormula(Var, A, Repl, NewA).
subInFormula(Var, neg A, Repl, neg NewA) :-
subInFormula(Var, A, Repl, NewA).
subInFormula(Var, A and B, Repl, NewA and NewB) :-
subInFormula(Var, A, Repl, NewA),
subInFormula(Var, B, Repl, NewB).
subInFormula(Var, A or B, Repl, NewA or NewB) :-
subInFormula(Var, A, Repl, NewA),
subInFormula(Var, B, Repl, NewB).
subInFormula(Var, A imp B, Repl, NewA imp NewB) :-
subInFormula(Var, A, Repl, NewA),
subInFormula(Var, B, Repl, NewB).
/* subInTerm(Var, Term, Repl, NewTerm) :-
the result of replacing all occurrences of variable Var
in justification term Term with occurrences of Repl
is NewTerm. Does not check that Var is a variable.
*/
subInTerm(Var, Var, Repl, Repl).
subInTerm(Var, Atom, _Repl, Atom) :-
atom(Atom), Atom \== Var.
subInTerm(Var, (One * Two), Repl, (NewOne * NewTwo)) :-
subInTerm(Var, One, Repl, NewOne),
subInTerm(Var, Two, Repl, NewTwo).
subInTerm(Var, (One + Two), Repl, (NewOne + NewTwo)) :-
subInTerm(Var, One, Repl, NewOne),
subInTerm(Var, Two, Repl, NewTwo).
/*************************************************************/
/* OTHER UTILITY METHODS USED BY CONVERSION PROCESS */
/* separateBinary(List, First, Second) :-
List is a list of binary formulas, all implications,
or all conjunctions, or all disjunctions. First becomes
the list of left components, and Second the list
of right components. Union is used to avoid repetitions.
*/
separateBinary([], [], []).
separateBinary([Binary | Rest], ListOne, ListTwo) :-
(Binary = A imp B; Binary = A and B; Binary = A or B),
separateBinary(Rest, RestOne, RestTwo),
union(RestOne, [A], ListOne),
union(RestTwo, [B], ListTwo).
/* separateNeg(List, NewList) :-
List is a list of negated formulas. NewList becomes
the list these formulas with negations removed.
Union is used to avoid repetitions.
*/
separateNeg([], []).
separateNeg([neg A | Rest], [A | NewRest]) :-
separateNeg(Rest, NewRest).
/* separateBox(List, NewList) :-
List is a list of formulas of the form t::A. NewList becomes
the list these formulas with t removed.
Union is used to avoid repetitions.
*/
separateBox([], []).
separateBox([_Term::A | Rest], [A | NewRest]) :-
separateBox(Rest, NewRest).
/* tBoxProcess(QuasiA, Aprime, SubstA, S) :-
QuasiA, Aprime, and SubstA are inputs. S is computed,
where S = t1 + … + tk as in the written version of the
algorithm. Recorded for use later is information written
as where(…), consisting of a new justification term, and
material from which the formula the term justifies can
be constructed. The formula is Aprime imp AiSubstA.
A constant t is also recorded to distinguish information
written by this case from that written by
fBoxProcess below.
*/
tBoxProcess([Ai], Aprime, SubstA, S) :-
gensym(t, Term),
S = Term,
assert(where(Term, Aprime, Ai, SubstA, t)).
tBoxProcess([Ai|Rest], Aprime, SubstA, S) :-
gensym(t, Term),
S = Term + RestS,
tBoxProcess(Rest, Aprime, SubstA, RestS),
assert(where(Term, Aprime, Ai, SubstA, t)).
/* fBoxProcess(QuasiSet, Aprime, SubstA, T) :-
QuasiSet, Aprime, and SubstA are inputs. T is
computed, where T = u1*t1 +…+ uk*tk as in the
written version of the algorithm. Recorded for
use later is information written as where(…),
consisting of a new justification term, and
material from which the formula the term justifies can
be constructed. The formula is \/AiSubstA imp Aprime.
A constant f is also recorded to distinguish information
written by this case from that written by
tBoxProcess above.
*/
fBoxProcess([Aterm::Adisj], Aprime, SubstA, T) :-
gensym(t, Term),
T = Term*Aterm,
assert(where(Term, Aprime, Adisj, SubstA, f)).
fBoxProcess([Aterm::Adisj|Rest], Aprime, SubstA, T) :-
gensym(t, Term),
T = (Term*Aterm) + RestS,
fBoxProcess(Rest, Aprime, SubstA, RestS),
assert(where(Term, Aprime, Adisj, SubstA, f)).
/* combineBoxDisj(InList, OutList, Type) :-
boxed disjunctions of InList are combined into
OutList, dropping the disjunctions and omitting
the boxes. Type is the kind of formula being
disjuncted. It uses disjunctToList, which see.
*/
combineBoxDisj([], [], _).
combineBoxDisj([_Term::Disj|Rest], List, Type) :-
disjunctToList(Disj, Temp1, Type),
combineBoxDisj(Rest, Temp2, Type),
union(Temp1, Temp2, List).
/* disjunctToList(Disjunct, List, Type) :-
Disjunct is a disjunction. List consists
of the formulas that are disjuncted, where
these are of type Type, taken to specify a
quasi-realization set. It is assumed that
the sign involved is f.
*/
disjunctToList(D, L, T) :- disjunctToList_(D, L, T), !.
disjunctToList_(A or Rest, List, T) :-
inQuasiSet(f(A), T),
disjunctToList_(Rest, Temp, T),
union(Temp, [A], List).
disjunctToList_(A, [A], _).
/* inQuasiSet(F,G) :-
signed justification formula F is a member
of <>, where G is a signed modal formula.
Indexes are suppressed in G.
*/
inQuasiSet(A, A) :- propAtom(A).
inQuasiSet(AlphaQ, AlphaF) :-
conjunctive(AlphaQ), conjunctive(AlphaF),
components(AlphaQ, AlphaQone, AlphaQtwo),
components(AlphaF, AlphaFone, AlphaFtwo),
inQuasiSet(AlphaQone, AlphaFone),
inQuasiSet(AlphaQtwo, AlphaFtwo).
inQuasiSet(BetaQ, BetaF) :-
disjunctive(BetaQ), disjunctive(BetaF),
components(BetaQ, BetaQone, BetaQtwo),
components(BetaF, BetaFone, BetaFtwo),
inQuasiSet(BetaQone, BetaFone),
inQuasiSet(BetaQtwo, BetaFtwo).
inQuasiSet(UnaryQ, UnaryF) :-
unary(UnaryQ), unary(UnaryF),
component(UnaryQ, CQ), component(UnaryF, CF),
inQuasiSet(CQ, CF).
inQuasiSet(t(_::Q), t(box F)) :-
inQuasiSet(t(Q), t(F)).
inQuasiSet(f(_::Q), f(box F)) :-
disjunctionFrom(f(Q), f(F)).
disjunctionFrom(A, F) :-
disjunctionFrom_(A, F), !.
disjunctionFrom_(f(Q), f(F)) :-
inQuasiSet(f(Q), f(F)).
disjunctionFrom_(f(A or B), f(F)) :-
inQuasiSet(f(A), f(F)),
disjunctionFrom_(f(B), f(F)).
/*************************************************************/
/* RUNNING AND DISPLAYING OUTPUT */
/* convert(QuasiSet, ModalFormula) :-
QuasiSet is a set of quasi-realizers, supplied as output
of a quasi-realization program. These are quasi-realizers
of ModalFormula. A realizer for ModalFormula is constructed
from QuasiSet, displayed, and then additional information
is displayed.
*/
convert(QuasiSet, ModalFormula) :-
reset,
condense(QuasiSet, f(ModalFormula), Realizer, _),
write('A realization is:'), nl, nl,
write(Realizer), nl, nl,
write('where:'), nl, nl,
writeReasons, nl.
writeReasons :-
where(Term, Aprime, Ai, SubstA, t),
sub(SubstA, Ai, AiSub),
write(Term::(Aprime imp AiSub)), nl, fail.
writeReasons :-
where(Term, Aprime, Adisj, SubstA, f),
sub(SubstA, Adisj, AdisjSub),
write(Term::(AdisjSub imp Aprime)), nl, fail.
writeReasons.
/***********************************************************/
/* TOP LEVEL DRIVER */
/***********************************************************/
/* realizer(ModalFormula, ModalDepth) :-
computes and displays information about a realizer for
ModalFormula. Quasi-realization information is also
displayed. A ModalDepth parameter must be supplied.
This is the maximum number of pi rule applications.
*/
realizer(ModalFormula, ModalDepth) :-
test(ModalFormula, ModalDepth, PassOn),
convert(PassOn, ModalFormula).