/*
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.
*/