% 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)).