Skip to content
Snippets Groups Projects
Commit baa07011 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add proof by refutation 


Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent b496aad0
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
logic_programming/3_PropositionalLogic.ipynb
+ 431
− 29
View file @ baa07011
%% Cell type:markdown id:9eb5530a tags:
# Propositional Logic
Syntax and Semantics Explained using a Prolog Implementation
%% Cell type:markdown id:dba70591 tags:
## Well-Formed Formulas (WFF)
All atomic propositions are WFF)
If a und b are WFF then so are:
- (¬ a)
- (a ∧ b)
- (a ∨ b)
- (a ⇒ b)
- (a ⟺ b)
No other formulas are WFF.
Comment: a, b are metavariablens outside the syntax of propositional logic.
%% Cell type:markdown id:dd01f86a tags:
Maybe this reminds you of formal grammars from a theoretical computer science lecture.
And indeed, the above can be written as a grammar using a non-terminal symbol wff.
In Prolog, grammars can actually be written using DCG notation, which we will see and understand much later in the course.
Here we simply write the grammar in Prolog style and can then use it to check if a formula is a WFF:
%% Cell type:code id:964ebd52 tags:
``` prolog
:- set_prolog_flag(double_quotes, codes).
wff --> "p". % atomic proposition
wff --> "q". % atomic proposition
wff --> "(¬",wff,")".
wff --> "(", wff, "∧", wff, ")".
wff --> "(", wff, "∨", wff, ")".
wff --> "(", wff, "⇒", wff, ")".
wff --> "(", wff, "⟺", wff, ")".
```
%% Cell type:code id:fc6823ad tags:
``` prolog
?- wff("p","").
```
%% Output
%% Cell type:code id:152289b6 tags:
``` prolog
?- wff("(¬p)","").
```
%% Output
%% Cell type:code id:2c3dd1bf tags:
``` prolog
?- wff("(p∧(q∨(¬p)))","").
%comment.
```
%% Output
%% Cell type:markdown id:38b0a282 tags:
This grammar does not talk about whitespace and requires parentheses for every connective used.
In practice, one typically uses operator precedences to avoid having to write too many parentheses:
- negation binds strongest
- then come conjunction and disjunction
- then come implication and equivalence.
So instead of
- (((¬ p) ∧ (¬ q)) ⇒ ((¬ p) ∨ (¬ q)))
we can write
- ¬ p ∧ ¬ q ⇒ ¬ p ∨ ¬ q
We will try not not mix conjunction/disjunction and implication/equivalence without parentheses.
We will also not try to improve our Prolog parser here to accomodate these precedences.
This is the subject of another course (on compiler construction).
%% Cell type:markdown id:92b6dc2d tags:
We will also see much later that Prolog allows one to annotate grammars with semantic values, here to generate
a Prolog term representing the logical formal in the form of a syntax tree:
%% Cell type:code id:78163b60 tags:
``` prolog
:- set_prolog_flag(double_quotes, codes).
wff(p) --> "p". % atomic proposition
wff(q) --> "q". % atomic proposition
wff(not(A)) --> "(¬",wff(A),")".
wff(and(A,B)) --> "(", wff(A), "∧", wff(B), ")".
wff(or(A,B)) --> "(", wff(A), "∨", wff(B), ")".
wff(impl(A,B)) --> "(", wff(A), "⇒", wff(B), ")".
wff(equiv(A,B)) --> "(", wff(A), "⟺", wff(B), ")".
```
%% Cell type:code id:8ddb568d tags:
``` prolog
?- wff(Formula,"(¬p)","").
```
%% Output
%% Cell type:code id:075dc3b2 tags:
``` prolog
?- wff(Formula,"(¬(p∧q))","").
```
%% Output
%% Cell type:code id:338cb7dd tags:
``` prolog
?- wff(Formula,"(p∧(q∨(¬p)))","").
```
%% Output
%% Cell type:markdown id:f9005519 tags:
The above Prolog term `and(p,or(q,not(p)))` represents the logical formula in tree form.
We can display the tree as a dag (directed acyclic graph) using the following subsidiary code
(in future the Jupyter kernel will probably have a dedicated command to show a term graphically):
%% Cell type:code id:f6116612 tags:
``` prolog
subtree(Term,Nr,SubTerm) :-
Term =.. [_|ArgList], %obtain arguments of the term
nth1(Nr,ArgList,SubTerm). % get sub-argument and its position number
% recursive and transitive closure of subtree
rec_subtree(Term,Sub) :- Term = Sub.
rec_subtree(Term,Sub) :- subtree(Term,_,X), rec_subtree(X,Sub).
subnode(Sub,[shape/S, label/F],Formula) :-
rec_subtree(Formula,Sub), % any sub-formula Sub of Formula is a node in the graphical rendering
functor(Sub,F,_), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect).
```
%% Cell type:code id:d7e68593 tags:
``` prolog
jupyter:print_table(subnode(Node,Dot,and(p,or(q,not(p)))))
```
%% Output
Node | Dot |
:- | :- |
and(p,or(q,not(p))) | [shape/rect,label/and] |
p | [shape/egg,label/p] |
or(q,not(p)) | [shape/rect,label/or] |
q | [shape/egg,label/q] |
not(p) | [shape/rect,label/not] |
p | [shape/egg,label/p] |
%% Cell type:code id:3646e3ee tags:
``` prolog
jupyter:show_graph(subnode(_,_,and(p,or(q,not(p)))),subtree/3)
```
%% Output
%% Cell type:markdown id:11b3a8ad tags:
Below we will study how one can assign a truth-value to logical formulas like the one above.
## Truth tables
Every logical connective has a truth table, indicating how it maps the truth of its arguments to its own truth value.
For example, `and` maps inputs `true` and `false` to `false`.
Below we encode the truth table for five connectives as Prolog facts and rules.
%% Cell type:code id:350b9756 tags:
``` prolog
not(true,false).
not(false,true).
and(true,V,V) :- truth_value(V).
and(false,V,false) :- truth_value(V).
or(true,V,true) :- truth_value(V).
or(false,V,V) :- truth_value(V).
implies(A,B,Res) :- not(A,NotA), or(NotA,B,Res).
equiv(A,B,Res) :- implies(A,B,AiB), implies(B,A,BiA), and(AiB,BiA,Res).
truth_value(true).
truth_value(false).
truth_table(A,B,NotA,AandB,AorB,AiB,AeB) :-
truth_value(A), truth_value(B),
not(A,NotA), and(A,B,AandB), or(A,B,AorB),
implies(A,B,AiB), equiv(A,B,AeB).
```
%% Cell type:markdown id:41cad0bc tags:
We can now use the predicates `and/3`, ... to compute the truth value of the connectives for a particular input:
%% Cell type:code id:3101448b tags:
``` prolog
?- and(true,false,X).
```
%% Output
%% Cell type:code id:922004e9 tags:
``` prolog
?- or(true,false,X).
```
%% Output
%% Cell type:markdown id:78c0eda3 tags:
We can also display the whole truth table using a Jupyter command:
%% Cell type:code id:54b57ff8 tags:
``` prolog
jupyter:print_table(truth_table(A,B,NotA,AandB,AorB,AimpliesB,AequivB))
```
%% Output
A | B | NotA | AandB | AorB | AimpliesB | AequivB |
:- | :- | :- | :- | :- | :- | :- |
true | true | false | true | true | true | true |
true | false | false | false | true | false | false |
false | true | true | false | true | true | false |
false | false | true | false | false | true | true |
%% Cell type:markdown id:ce32b1d0 tags:
An <b>interpretation</b> is an assignment of all relevant proposition to truth values (true or false).
For example, given the formula `(p∧(q∨(¬p)))` an interpretation needs to assign a truth value to `p` and `q`.
In the Prolog code below we will represent an interpretation as a list of bindings, each binding is a term of the form `Proposition/TruthValue`.
For example, one of the four possible interpretations for the formula above is `[p/true, q/false]`.
Using the built-in `member/2` predicate we can inspect an interpretation in Prolog. For example, here we retrieve the truth value of `q`:
%% Cell type:code id:8f6d804b tags:
``` prolog
?- Interpetation=[p/true, q/false], member(q/Q,Interpetation).
```
%% Output
%% Cell type:markdown id:0d236e48 tags:
Given an interpretation we can now compute the truth value for an entire formula in a recursive fashion.
For propositions we look up the truth value in the interpretation (done using `member` below).
For logical connectives we recursively compute the truth value of its arguments and then apply the truth tables we defined above.
%% Cell type:code id:175c00d0 tags:
``` prolog
value(X,Interpretation,Value) :-
atomic(X), % we have a proposition
member(X/Value,Interpretation).
value(and(A,B),I,Val) :- value(A,I,VA), value(B,I,VB),
and(VA,VB,Val).
value(or(A,B),I,Val) :- value(A,I,VA), value(B,I,VB),
or(VA,VB,Val).
value(not(A),I,Val) :- value(A,I,VA),
not(VA,Val).
value(implies(A,B),I,Val) :- value(or(not(A),B),I,Val).
value(equiv(A,B),I,Val) :-
value(and(implies(A,B),implies(B,A)),I,Val).
```
%% Cell type:markdown id:aa50ec0e tags:
Using the above we can compute the truth value of `(p∧(q∨(¬p)))` for the interpretation `[p/true, q/false]`:
%% Cell type:code id:eee17774 tags:
``` prolog
?- value(and(p,or(q,not(p))), [p/true, q/false],Res).
```
%% Output
%% Cell type:markdown id:4387b4a2 tags:
The truth value of `(p∧(q∨(¬p)))` for the interpretation `[p/true, q/true]` is true.
In this case the interpretation is called a <b>model</b> of the formula.
%% Cell type:code id:fec75f65 tags:
``` prolog
?- value(and(p,or(q,not(p))), [p/true, q/true],Res).
```
%% Output
%% Cell type:markdown id:3aa46665 tags:
We can also compute the truth table of the entire formula, by trying out all possible interpretations.
Below we leave P and Q as Prolog variable which is instantiated by the code above:
%% Cell type:code id:78473da0 tags:
``` prolog
jupyter:print_table(value(and(p,or(q,not(p))), [p/P, q/Q],Res))
```
%% Output
P | Q | Res |
:- | :- | :- |
true | true | true |
true | false | false |
false | true | false |
false | false | false |
%% Cell type:markdown id:5b4ee42b tags:
Below we visualise graphically this computation, by displaying the syntax tree of a logical formula
as a dag and by colouring the nodes using the `value` predicate:
%% Cell type:code id:2ee60c15 tags:
``` prolog
subnode_val(Sub,[shape/S, label/F, style/filled, fillcolor/C],Formula,Interpretation) :-
rec_subtree(Formula,Sub), % any sub-formula Sub of Formula is a node in the graphical rendering
functor(Sub,F,_), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect),
(value(Sub,Interpretation,true) -> C=olive ; C=sienna1).
```
%% Cell type:code id:2b497dad tags:
``` prolog
jupyter:show_graph(subnode_val(_,_,and(p,or(q,not(p))),[p/true,q/false]),subtree/3)
```
%% Output
%% Cell type:code id:0fd23f05 tags:
``` prolog
jupyter:show_graph(subnode_val(_,_,and(p,or(q,not(p))),[p/true,q/true]),subtree/3)
```
%% Output
%% Cell type:markdown id:013fda69 tags:
A formula for which all interpretations are models is called a <b>tautology</b>:
%% Cell type:code id:23775624 tags:
``` prolog
jupyter:print_table(value(or(p,not(p)), [p/P],Res))
```
%% Output
P | Res |
:- | :- |
true | true |
false | true |
%% Cell type:code id:7a6e29ed tags:
``` prolog
jupyter:print_table(value(or(p,or(q,not(q))), [p/P, q/Q],Res))
```
%% Output
P | Q | Res |
:- | :- | :- |
true | true | true |
false | true | true |
true | false | true |
false | false | true |
%% Cell type:markdown id:9ff1936a tags:
A formula which has no models is called a <b>contradiction</b>:
%% Cell type:code id:6bd292f4 tags:
``` prolog
jupyter:print_table(value(and(p,not(p)), [p/P],Res))
```
%% Output
P | Res |
:- | :- |
true | false |
false | false |
%% Cell type:markdown id:fc920c04 tags:
A formula which has at least one model is called <b>satisfiable</b>.
We can use our code above to find models, by leaving the interpretation of propositions as Prolog variables
and by requiring the result to be `true`:
%% Cell type:code id:ab15628a tags:
``` prolog
?-value(and(p,or(q,not(p))), [p/P, q/Q],true).
```
%% Output
%% Cell type:markdown id:64baad25 tags:
The above is not a very efficient way of finding models.
We return to this issue later.
A tool that determines whehter a propositional logic formula is satisfiable and computes possibles models is called a <b>SAT solver</b>.
%% Cell type:markdown id:8b2acc10 tags:
Two formulas are called <b>equivalent</b> iff they have the same models:
%% Cell type:code id:b912acd3 tags:
``` prolog
jupyter:print_table(value(or(not(p),q), [p/P, q/Q],Res))
```
%% Output
P | Q | Res |
:- | :- | :- |
true | true | true |
true | false | false |
false | true | true |
false | false | true |
%% Cell type:code id:f4c9823d tags:
``` prolog
jupyter:print_table(value(implies(p,q), [p/P, q/Q],Res))
```
%% Output
P | Q | Res |
:- | :- | :- |
true | true | true |
true | false | false |
false | true | true |
false | false | true |
%% Cell type:code id:68a2a19c tags:
``` prolog
jupyter:print_table((user:value(or(not(p),q), [p/P, q/Q],NotPandQ),user:value(implies(p,q), [p/P, q/Q],PimpliesQ)))
```
%% Output
P | Q | NotPandQ | PimpliesQ |
:- | :- | :- | :- |
true | true | true | true |
true | false | false | false |
false | true | true | true |
false | false | true | true |
%% Cell type:markdown id:248d3d32 tags:
A formula `B` is the logical consequence of `A` if all models of `A` are also models of `B`:
%% Cell type:code id:aaf46953 tags:
``` prolog
jupyter:print_table((user:value(and(p,q), [p/P, q/Q],PandQ),user:value(or(p,q), [p/P, q/Q],PorQ)))
```
%% Output
P | Q | PandQ | PorQ |
:- | :- | :- | :- |
true | true | true | true |
true | false | false | true |
false | true | false | true |
false | false | false | false |
%% Cell type:markdown id:3e261892 tags:
## Improving our Prolog program
For convenience we now write some piece of Prolog code to find the atomic propositions used within a formula.
This obviates the need to write interpretation skeletons like `[p/P,q/Q]` ourselves.
%% Cell type:code id:da0a82b5 tags:
``` prolog
get_aps(Formula,SortedPropositions) :- findall(P, ap(Formula,P), Ps), sort(Ps,SortedPropositions).
% extract atomic propostions used by formula
ap(X,X) :- atomic(X).
ap(and(A,B),AP) :- ap(A,AP) ; ap(B,AP).
ap(or(A,B),AP) :- ap(A,AP) ; ap(B,AP).
ap(implies(A,B),AP) :- ap(A,AP) ; ap(B,AP).
ap(equiv(A,B),AP) :- ap(A,AP) ; ap(B,AP).
ap(not(A),AP) :- ap(A,AP).
```
%% Cell type:code id:82980216 tags:
``` prolog
?- get_aps(and(p,q),Ps).
```
%% Output
%% Cell type:markdown id:e4c2468b tags:
We can now write a more convenient predicate to find models for a formula:
%% Cell type:code id:23cfb806 tags:
``` prolog
sat(Formula,Interpretation) :-
get_aps(Formula,SPs),
skel(SPs,Interpretation), % set up interpretation skeleton
value(Formula,Interpretation,true).
skel([],[]).
skel([AP|T],[AP/_|ST]) :- skel(T,ST). % we replace p by p/_ so that we have an unbound logical varible for every proposition
unsat(Formula) :- \+ sat(Formula,_). % a formula is unsatisfiable if we can find no model, \+ is Prolog negation
```
%% Cell type:code id:6338f6bf tags:
``` prolog
?- sat(and(p,or(q,not(p))),Model).
```
%% Output
%% Cell type:code id:266a4bd8 tags:
``` prolog
?- unsat(and(p,not(p))).
```
%% Output
%% Cell type:markdown id:9fb0715e tags:
## Proof by contradiction
To prove that `B` is a logical consequence of `A` we can employ a <b>proof by contradiction</b>:
- assume that `B` is false and
- show that this leads to a contradiction.
%% Cell type:code id:6957d9f3 tags:
``` prolog
prove(A,B) :- /* prove that B follows from A */
unsat(and(A,not(B))).
```
%% Cell type:code id:f552a71e tags:
``` prolog
?- prove(and(p,q),or(p,q)).
```
%% Output
%% Cell type:code id:e7a2828d tags:
``` prolog
?- prove(or(p,q),and(p,q)).
```
%% Output
%% Cell type:markdown id:02395cde tags:
In case something is not a logical consequence we can use this code to find an explanation (aka counter example):
%% Cell type:code id:26bab55b tags:
``` prolog
disprove(A,B,CounterExample) :- /* show why B does not follow from A */
sat(and(A,not(B)),CounterExample).
```
%% Cell type:code id:fe5daeb4 tags:
``` prolog
?- disprove(or(p,q),and(p,q),Counter).
```
%% Output
%% Cell type:code id:3187bee7 tags:
``` prolog
```
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment