/* Author: MB Version: JUL 2016 Modelling an adaptive logic which is paraconsistent and allows for versions of default reasoning. A derivation consists of a numbered lists of lines. Each line contains: a number, a list of assumptions it depends on, the sentence derived, the justification, the list of presuppositions, and a list of defeaters of (some) presupposition (i.e. a list of line numbers of lines which were used in cancelling a presupposition). As defeaters can be defeated a line can be restated. Newly derived lines have empty defeater sets. We derive only from non-defeated lines. derived(Number,Assumptions,Sentence,Justification,Presuppositions,Defeaters) Derived lines inherit the assumptions and presuppositions of the lines they are derived from. Thus in case of retraction they are directly affected (the crucial sentence belongs to their own presupposition set). Presuppositions can be cancelled by lines which are not sharing assumptions, as new information (i.e. new assumptions) can lead to cancellation of presuppositions. We can also derive lines from lines with an empty defeater set. Complex sentences are expressed by predicates: conjunction(X,Y), disjunction(X,Y), negation(X), implication(X,Y) Justifications are expressed like natural deduction rules: conjunctionElimination, conjunctionIntroduction etc. Presuppositions contains the sentences which should not be derived otherwise the line in question has to be retracted. Types of presuppositions: consistent(X) */ :- dynamic derived/5. :- dynamic numberOfLines/1. % I. Setup of derivation numberOfLines(0). % we have to count the lines, a global variable objects([a]). % there is at least one object % II. Logical rules % Negation Elimination (Double Negation Elimination) derived(N,Assumptions,Line,Justification,Presuppositions,[]):- derived(N1,Assumptions,negation(negation(Line)),_,Presuppositions,[]), Justification = negationElimination(N1), addLine(N,Assumptions,Line,Justification,Presuppositions,[]). % Negation Introduction (paraconsistent version) derived(N,Assumptions,negation(Line1),Justification,Presuppositions,[]):- derived(N1,AssumptionsN1,LineN1,_,PresuppositionsN1,[]), derived(N2,AssumptionsN2,negation(LineN1),_,PresuppositionsN2,[]), member(LineN1,AssumptionsN2), Justification = negationIntroduction(N1,N2), append(PresuppositionsN1,PresuppositionsN2,PresuppositionsN), dupplicateElimination(PresuppositionsN,[],Presuppositions), deleteElement(LineN1,AssumptionsN2,AssumptionsN2New), append(AssumptionsN1,AssumptionsN2New,AssumptionsN), dupplicateElimination(AssumptionsN,[],Assumptions), addLine(N,Assumptions,negation(Line1),Justification,Presuppositions,[]). % Conjunction Elimination derived(N,Assumptions,Line,Justification,Presuppositions,[]):- derived(N1,Assumptions,LineN1,_,Presuppositions,[]), Justification = conjunctionElimination(N1), (LineN1 = conjunction(_,Line); LineN1 = conjunction(Line,_)), addLine(N,Assumptions,Line,Justification,Presuppositions,[]). % Conjunction Introduction derived(N,Assumptions,Line,Justification,Presuppositions,[]):- derived(N1,AssumptionsN1,LineN1,_,PresuppositionsN1,[]), derived(N2,AssumptionsN2,LineN2,_,PresuppositionsN2,[]), Justification = conjunctionIntroduction(N1,N2), (Line = conjunction(LineN1,LineN2); Line = conjunction(LineN2,LineN1)), append(AssumptionsN1,AssumptionsN2,AssumptionsN3), dupplicateElimination(AssumptionsN3,[],Assumptions), append(PresuppositionsN1,PresuppositionsN2,PresuppositionsN3), dupplicateElimination(PresuppositionsN3,[],Presuppositions), addLine(N,Assumptions,Line,Justification,Presuppositions,[]). % Disjunction Introduction derived(N,Assumptions,Line,Justification,Presuppositions,[]):- derived(N1,Assumptions,LineN1,_,Presuppositions,[]), Justification = disjunctionIntroduction(N1), % arbitrary non-relevant addition! (Line = disjunction(LineN1,_); Line = disjunction(_,LineN1)), addLine(N,Assumptions,Line,Justification,Presuppositions,[]). % Disjuntion Elimination derived(N,Assumptions,Line,Justification,Presuppositions,[]):- derived(N1,AssumptionsN1,disjunction(LineN2,Line),_,PresuppositionsN1,[]), derived(N2,AssumptionsN2,negation(LineN2),_,PresuppositionsN2,[]), Justification = disjunctionElimination(N1,N2), append(PresuppositionsN1,PresuppositionsN2,PresuppositionsTemp), append(PresuppositionsTemp,[consistent(LineN2)],PresuppositionsN), dupplicateElimination(PresuppositionsN,[],Presuppositions), append(AssumptionsN1,AssumptionsN2,AssumptionsN), dupplicateElimination(AssumptionsN,[],Assumptions), addLine(N,Assumptions,Line,Justification,Presuppositions,[]). % Implication Elimination (Modus Ponens), a variant of Disjunction Elimination derived(N,Assumptions,Line,Justification,Presuppositions,[]):- derived(N1,AssumptionsN1,implication(LineN2,Line),_,PresuppositionsN1,[]), derived(N2,AssumptionsN2,LineN2,_,PresuppositionsN2,[]), Justification = implicationElimination(N1,N2), append(PresuppositionsN1,PresuppositionsN2,PresuppositionsTemp), append(PresuppositionsTemp,[consistent(LineN2)],PresuppositionsN), dupplicateElimination(PresuppositionsN,[],Presuppositions), append(AssumptionsN1,AssumptionsN2,AssumptionsN), dupplicateElimination(AssumptionsN,[],Assumptions), addLine(N,Assumptions,Line,Justification,Presuppositions,[]). % Implication Introduction (Deduction Theorem) derived(N,Assumptions,implication(LineN1,LineN2),Justification,Presuppositions,[]):- derived(N1,AssumptionsN1,LineN1,_,PresuppositionsN1,[]), derived(N2,AssumptionsN2,LineN2,_,PresuppositionsN2,[]), member(LineN1,AssumptionsN2), Justification = implicationIntroduction(N1,N2), append(PresuppositionsN1,PresuppositionsN2,PresuppositionsN), dupplicateElimination(PresuppositionsN,[],Presuppositions), deleteElement(LineN1,AssumptionsN2,AssumptionsN2New), append(AssumptionsN1,AssumptionsN2New,AssumptionsN), dupplicateElimination(AssumptionsN,[],Assumptions), addLine(N,Assumptions,implication(LineN1,LineN2),Justification,Presuppositions,[]). % III. Dynamic Rules retraction(Line):- % sofar the line to be retracted was derivable derived(N,Assumptions,LineN,Justification,Presuppositions,[]), member(P,Presuppositions), negates(Line,P), retract(derived(N,_,_,_,_,_)), % if the defeated line defeated other lines they are available again recomputeDefeat(LineN), % flagged by its defeater assert(derived(N,Assumptions,LineN,Justification,Presuppositions,[Line])). retraction(Line):- % this line is already flagged derived(N,Assumptions,LineN,Justification,Presuppositions,Defeaters), Defeaters \= [], member(P,Presuppositions), negates(Line,P), retract(derived(N,_,_,_,_,_)), append(Defeaters,[Line],NewDefeaters), assert(derived(N,Assumptions,LineN,Justification,Presuppositions,NewDefeaters)). % flagged by all its defeaters recomputeDefeat(Line):- derived(N,Assumptions,LineN,Justification,Presuppositions,Defeaters), member(Line,Defeaters), deleteElement(Line,Defeaters), Defeaters = [], retract(derived(N,_,_,_,_,_)), assert(derived(N,Assumptions,LineN,Justification,Presuppositions,[])). recomputeDefeat(Line):- derived(N,Assumptions,LineN,Justification,Presuppositions,Defeaters), member(Line,Defeaters), deleteElement(Line,Defeaters), Defeaters \= [], % but other defeaters left in place retract(derived(N,_,_,_,_,_)), assert(derived(N,Assumptions,LineN,Justification,Presuppositions,Defeaters)). % IV. Structural predicates for building a derivation addLine(N,Assumptions,Line,Justification,Presuppositions,Defeaters):- increaseNumberOfLines(N), assert(derived(N,Assumptions,Line,Justification,Presuppositions,Defeaters)), retraction(Line). increaseNumberOfLines(N):- numberOfLines(Y), N is Y + 1, retract(numberOfLines(_)), assert(numberOfLines(N)). negates(conjunction(X,negation(X)),consistent(X)). % V. Additional predicates deleteElement(X,[X],[]). deleteElement(X,[X|L],M) :- deleteElement(X,L,M). deleteElement(X,[Y|L1],[Y|L2]) :- deleteElement(X,L1,L2). duplicateElimination([],A,A). duplicateElimination([H|T],A,L) :- member(H,A), !, duplicateElimination(T,A,L). duplicateElimination([H|T],A,L) :- duplicateElimination(T,[H|A],L). % VI. Initialisation (by assumptions and/or axioms/theorems) /* Making an Assumption use: addLine(N,[Line],Line,assumption,[],[]). */ /* Introducing an axiom (or known theorem) use: addLine(N,[],Line,axiom/theorem,[],[]). */ init:- addLine(N,[],a=a,axiom,[],[]). /* Further Remarks This assumes we try to test whether some formula is derivable (has been derived) by testing the goal state of its being derived (given maybe assumptions etc.). We get the information whether the formula can be derived, we do not receive the proof. We thus reason backwards. Reasoning forwards would generate a manifold of ever more complex but useless formulae. Without further ordering of logical rules all conjunctions would be produced first. */