% Copy this text into your PROLOG editor and consult/compile
%
% SINCE THIS STILL DOES NOT WORK PERFECTLY, HAVE A TRY AT IT!
%
% Author: Manuel Bremer
% Heinrich-Heine-Universität Düsseldorf, Germany
% Date: 2005
% Title: (SWI)-PROLOG Implementation of (propositional) LP decision procedure
%
% This file implements a straight forward tree decision procedure for
% propositional LP in PROLOG. Connectives and truth values are defined as
% PROLOG predicates, only in satisfying the (Horn-)clauses for these predicates
% and backtracking the underlying logic of PROLOG is used.
%
% To speed up the procedure assertions concerning already visited parts of a
% decision tree are used (otherwise the procedure is of exponential complexity).
% The SWI-PROLOG inbuild predicate "retractall" is used; in other PROLOG
% versions it has to be simulated using "retract" and "fail". A second set of
% assertions is used to check the value assignments on branches for
% compatibility.
% The program is run by typing "runTheorem." or "runConsequence." at the
% interpreter. In case of checking a single sentence one is asked for the
% formula to be checked. The formula should be entered in the format defined
% here ENDING WITH A FULL STOP and using the "ENTER" key.
% If the formula can be assigned the given truth value PROLOG yields the
% respective evaluations, otherwise answers "No." So testing for "OnlyFalse(..)"
% with a "No"-answer reveals the tested sentence as a LP-theorem.
% In case of checking a supposed consequence relationship one is prompted for
% the premises as well as the consequent. Premises have to be entered as a list.
%
% On the corresponding trees and LP in general see:
% Bremer, Manuel. An Introduction to Paraconsistent Logics. New York et al.,
% 2005, Chap. 4.
%
:- dynamic onlyFals/1, onlyFalse/1 .
:- dynamic onlyTru/1, onlyTrue/1 .
:- dynamic atLeastTru/1, atLeastTrue/1 .
:- dynamic atLeastFals/1, atLeastFalse/1 .
runTheorem:-
retractall(onlyTru(_)), % clearing added formulas from the last run
retractall(onlyFals(_)), % used in the compatibility lists
retractall(atLeastTru(_)),
retractall(atLeastFals(_)),
retractall(onlyTrue(_)), % clearing added formulas from the last run
retractall(onlyFalse(_)), % used for speed up [at the moment mostly
retractall(atLeastTrue(_)), % overriden by "fail"-construction!]
retractall(atLeastFalse(_)),
assertz(onlyTru(verum)), % avoiding having empty lists of evaluated
% constants, this is not necessary, but may
% help in tracing to identify lists
assertz(atLeastTru(liar)),
assertz(onlyFals(falsum)),
assertz(atLeastFals(liar)),
write('Formulas look like "or(and(X,Y),if(Z,non(W)))".'), nl,
write('Which formula should be tested?'), nl,
read(Formula),
onlyFalse(Formula), % building up the tree
evaluateTree, % checking incompatible evaluations on the tree
fail. % force backtracking for disjunctions
runTheorem:- true.
runConsequence:-
retractall(onlyTru(_)),
retractall(onlyFals(_)),
retractall(atLeastTru(_)),
retractall(atLeastFals(_)),
retractall(onlyTrue(_)),
retractall(onlyFalse(_)),
retractall(atLeastTrue(_)),
retractall(atLeastFalse(_)),
assertz(onlyTru(verum)),
assertz(atLeastTru(liar)),
assertz(onlyFals(falsum)),
assertz(atLeastFals(liar)),
write('Formulas look like "or(and(X,Y),if(Z,non(W)))".'), nl,
write('Include multiple premises into square brackets and separate '),
write('them by commata, like "[or(A,B),non(A)]".'), nl,
write('Which premises should be used?'), nl,
read(Formula1),
checkPremiseSet(Formula1), % trying to have the premises being true
write('Which consequence should follow?'), nl,
read(Formula2),
onlyFalse(Formula2),
% building up the tree for supposed consequence, whether falsifying
% succeeds or not, otherwise evaluation cannot be displayed
evaluateTree, % checking incompatible evaluations on the tree
fail. % force backtracking for disjunctions
runConsequence:- true.
checkPremiseSet([Formula]) :- atLeastTrue(Formula).
checkPremiseSet([Head|Body]) :- atLeastTrue(Head),
checkPremiseSet(Body).
checkPremiseSet([]) :- atLeastTrue(liar). % just in case of input error
evaluateTree:-
write('Entering checking the consistency of the generated tree.'), nl,
% Note: the facts asserted on run-time use predicates shortened in spelling
% to avoid exception with the rules for the truth value predicates
findall(SimpleTruth,onlyTru(SimpleTruth),SimpleTruthsList),
findall(SimpleFalsehood,onlyFals(SimpleFalsehood),SimpleFalsehoodList),
findall(Truths,atLeastTru(Truths),TruthsList),
findall(Falsehoods,atLeastFals(Falsehoods),FalsehoodList),
compareList(SimpleTruthsList, FalsehoodList,Result1),
compareList(SimpleTruthsList, SimpleFalsehoodList, Result2),
compareList(SimpleFalsehoodList, TruthsList, Result3),
checkResults(Result1,Result2,Result3,Result),
communicate(Result).
checkResults(Result1, Result2, Result3, Result) :-
Result1 = Result2,
Result2 = Result3,
Result = Result1.
checkResults(_,_,_,not(true)).
communicate(Result) :- Result = not(true), !,
write('The formula/consequence cannot be made false only!'),
nl,
write('Another branch may be checked now.'),
nl,
write('The formula, so far, IS a LP-Theorem/Consequence!').
communicate(true) :- write('The formula/consequence tested IS NOT LP-valid!'),
!, nl,
displayTree.
compareList([Head|_],List,Result) :-
member(Head,List), !,
Result = not(true).
compareList([_|Body],List,Result) :-
compareList(Body,List,Result).
compareList([],_,Result) :- Result = true.
displayTree:- write('The formula is invalidated by the evaluation: '), nl,
write('Make false only: '), nl,
findall(SimpleFalsehood,onlyFals(SimpleFalsehood),SimpleFalsehoodList),
printAtomic(SimpleFalsehoodList), nl,
write('Make true only: '), nl,
findall(SimpleTruth,onlyTru(SimpleTruth),SimpleTruthsList),
printAtomic(SimpleTruthsList), nl,
write('Make at least true: '), nl,
findall(Truths,atLeastTru(Truths),TruthsList),
printAtomic(TruthsList), nl,
write('And make at least false: '), nl,
findall(Falsehoods,atLeastFals(Falsehoods),FalsehoodList),
printAtomic(FalsehoodList).
printAtomic([Head|Body]) :- atomic(Head), !,
write(Head), write(' '),
printAtomic(Body).
printAtomic([_|Body]) :- printAtomic(Body).
printAtomic([]).
% Going through the cases for the value "OnlyFalse",
% for the other truth values accordingly
onlyFalse(X) :- atomic(X), asserta(onlyFals(X)).
% i.e. propositional constant evaluated as being only false
onlyFalse(X) :- functor(X,Y,_),
Y = non, % formula to be checked is a negation
write('Negation checked.'), nl, !, % tells us where we are
arg(1,X,A), % "A" being the formula negated in "X"
onlyTrue(A), % condition to be checked now
asserta(onlyFals(X)), % keeping the result to avoid computing
asserta(onlyFalse(X)). % it once again if needed
onlyFalse(X) :- functor(X,Y,_),
Y = and, % formula to be checked is a conjunction
write('Conjunction checked'), nl,
arg(1,X,A),
arg(2,X,B), % the conjuncts
(onlyFalse(A); onlyFalse(B)),
% one of the conjuncts has to be only false
asserta(onlyFals(X)),
asserta(onlyFalse(X)).
onlyFalse(X) :- functor(X,Y,_),
Y = or, % formula to be checked is a disjunction
write('Disjunction checked'), nl, !,
arg(1,X,A),
arg(2,X,B), % the disjuncts
onlyFalse(A), % both disjuncts need to be false only
onlyFalse(B),
asserta(onlyFals(X)),
asserta(onlyFalse(X)).
onlyFalse(X) :- functor(X,Y,_),
Y = if, % formula to be checked is a conditional
write('Conditional checked'), nl, !,
arg(1,X,A), % antecedent
arg(2,X,B), % consequent
onlyTrue(A), % conditional is onlyFalse if antecedent is
onlyFalse(B), % onlyTrue and consequent is OnlyFalse
asserta(onlyFals(X)),
asserta(onlyFalse(X)).
onlyFalse(X) :- functor(X,Y,_),
Y = iff, % formula to be checked is a bi-conditional
write('Biconditional checked'), nl,
arg(1,X,A),
arg(2,X,B), % the two sides of the bi-conditional
% two sides need to have incompatible truth values
((onlyFalse(A), onlyTrue(B));(onlyTrue(A),onlyFalse(B))),
asserta(onlyFals(X)),
asserta(onlyFalse(X)).
atLeastFalse(X) :- atomic(X), asserta(atLeastFals(X)).
atLeastFalse(X) :- functor(X,Y,_),
Y = non, % formula to be checked is a negation
write('Negation checked.'), nl, !, % tells us where we are
arg(1,X,A), % "A" being the formula negated in "X"
atLeastTrue(A), % condition to be checked now
asserta(atLeastFals(X)),
asserta(atLeastFalse(X)).
atLeastFalse(X) :- functor(X,Y,_),
Y = and, % formula to be checked is a conjunction
write('Conjunction checked'), nl,
arg(1,X,A),
arg(2,X,B), % the conjuncts
(atLeastFalse(A); atLeastFalse(B)),
% one of the conjuncts has to be false
asserta(atLeastFals(X)),
asserta(atLeastFalse(X)).
atLeastFalse(X) :- functor(X,Y,_),
Y = or, % formula to be checked is a disjunction
write('Disjunction checked'), nl, !,
arg(1,X,A),
arg(2,X,B), % the disjuncts
atLeastFalse(A), % both disjuncts need to be false
atLeastFalse(B),
asserta(atLeastFals(X)),
asserta(atLeastFalse(X)).
atLeastFalse(X) :- functor(X,Y,_),
Y = if, % formula to be checked is a conditional
write('Conditional checked'), nl, !,
arg(1,X,A), % antecedent
arg(2,X,B), % consequent
atLeastTrue(A), % conditional is false if antecedent is
atLeastFalse(B), % true and consequent is false
asserta(atLeastFals(X)),
asserta(atLeastFalse(X)).
atLeastFalse(X) :- functor(X,Y,_),
Y = iff, % formula to be checked is a bi-conditional
write('Biconditional checked'), nl,
arg(1,X,A),
arg(2,X,B), % the two sides of the bi-conditional
% two sides need to have different truth values
((atLeastFalse(A), atLeastTrue(B));
(atLeastTrue(A),atLeastFalse(B))),
asserta(atLeastFals(X)),
asserta(atLeastFalse(X)).
onlyTrue(X) :- atomic(X), asserta(onlyTru(X)).
onlyTrue(X) :- functor(X,Y,_),
Y = non,
write('Negation checked'), nl, !,
arg(1,X,A),
onlyFalse(A),
asserta(onlyTru(X)),
asserta(onlyTrue(X)).
onlyTrue(X) :- functor(X,Y,_),
Y = and,
write('Conjunction checked'), nl, !,
arg(1,X,A),
arg(2,X,B), % the conjuncts
onlyTrue(A),
onlyTrue(B), % both of the conjuncts have to be only true
asserta(onlyTru(X)),
asserta(onlyTrue(X)).
onlyTrue(X) :- functor(X,Y,_),
Y = or, % formula to be checked is a disjunction
write('Disjunction checked'), nl,
arg(1,X,A),
arg(2,X,B), % the disjuncts
(onlyTrue(A); onlyTrue(B)), % one disjunct has to be only true
asserta(onlyTru(X)),
asserta(onlyTrue(X)).
onlyTrue(X) :- functor(X,Y,_),
Y = if, % formula to be checked is a conditional
write('Conditional checked'), nl,
arg(1,X,A), % antecedent
arg(2,X,B), % consequent
(onlyFalse(A); onlyTrue(B)), % conditional is onlyTrue if either
% antecedent is onlyFalse or
% consequent is onlyTrue
asserta(onlyTru(X)),
asserta(onlyTrue(X)).
onlyTrue(X) :- functor(X,Y,_),
Y = iff, % formula to be checked is a bi-conditional
write('Biconditional checked'), nl,
arg(1,X,A),
arg(2,X,B), % the two sides of the bi-conditional
% two sides need to have the same strict truth value
((onlyTrue(A), onlyTrue(B));(onlyFalse(A),onlyFalse(B))),
asserta(onlyTru(X)),
asserta(onlyTrue(X)).
atLeastTrue(X) :- atomic(X), asserta(atLeastTru(X)).
atLeastTrue(X) :- functor(X,Y,_),
Y = non, % formula to be checked is a negation
write('Negation checked'), nl, !, % tells us where we are
arg(1,X,A), % "A" being the formula negated in "X"
atLeastFalse(A), % condition to be checked now
asserta(atLeastTru(X)),
asserta(atLeastTrue(X)).
atLeastTrue(X) :- functor(X,Y,_),
Y = and, % formula to be checked is a conjunction
write('Conjunction checked'), nl, !,
arg(1,X,A),
arg(2,X,B), % the conjuncts
atLeastTrue(A),
atLeastTrue(B), % both of the conjuncts have to be true
asserta(atLeastTru(X)),
asserta(atLeastTrue(X)).
atLeastTrue(X) :- functor(X,Y,_),
Y = or, % formula to be checked is a disjunction
write('Disjunction checked'), nl,
arg(1,X,A),
arg(2,X,B), % the disjuncts
(atLeastTrue(A); atLeastTrue(B)), % one disjunct has to be true
asserta(atLeastTru(X)),
asserta(atLeastTrue(X)).
atLeastTrue(X) :- functor(X,Y,_),
Y = if, % formula to be checked is a conditional
write('Conditional checked'), nl,
arg(1,X,A), % antecedent
arg(2,X,B), % consequent
(atLeastFalse(A); atLeastTrue(B)), % conditional is true if either
% antecedent is false or
% consequent is true
asserta(atLeastTru(X)),
asserta(atLeastTrue(X)).
atLeastTrue(X) :- functor(X,Y,_),
Y = iff, % formula to be checked is a bi-conditional
write('Biconditional checked'), nl,
arg(1,X,A),
arg(2,X,B), % the two sides of the bi-conditional
% two sides need to have the same truth value
((atLeastTrue(A), atLeastTrue(B));
(atLeastFalse(A),atLeastFalse(B))),
asserta(atLeastTru(X)),
asserta(atLeastTrue(X)).