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

change implication arrow 


Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent d661ab89
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
+ 136
− 143
View file @ d04843d9
%% 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)
- (a ⟺ b)
No other formulas are WFF.
Note in the slides we use the single arrow `→` instead of the double arrow `⇒` for implication.
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, ")".
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)))
- (((¬ p) ∧ (¬ q)) → ((¬ p) ∨ (¬ q)))
we can write
- ¬ p ∧ ¬ q ⇒ ¬ p ∨ ¬ q
- ¬ 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(impl(A,B)) --> "(", wff(A), "→", wff(B), ")".
wff(equiv(A,B)) --> "(", wff(A), "⟺", wff(B), ")".
parse_wff(String,Formula) :- wff(Formula,String,"").
```
%% Cell type:code id:6b9c3364 tags:
``` prolog
?- parse_wff("(¬p)",Formula).
```
%% Output
%% Cell type:code id:075dc3b2 tags:
``` prolog
?- parse_wff("(¬(p∧q))",Formula).
```
%% Output
%% Cell type:code id:338cb7dd tags:
``` prolog
?- parse_wff("(p∧(q∨(¬p)))",Formula).
```
%% 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:f3c2de52 tags:
We can also use our parser instead of writing the logical formulas as Prolog terms:
%% Cell type:code id:575fc20f tags:
``` prolog
?- parse_wff("(p∧(q∨(¬p)))",Formula), value(Formula, [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 |
Two formulas are called <b>equivalent</b> iff they have the same models.
We write this as `A ≡ B`.
Below we can see that the models of `¬p ∨ q` and `p → q` are identical,
i.e., `¬p ∨ q ≡ p → q`.
%% 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`:
A formula `B` is the logical consequence of `A` if all models of `A` are also models of `B`.
We write this as `A ⊨ B`.
Below we can see that all models of `p ∧ q` are also models of `p ∨ q`,
i.e., `p ∧ q ⊨ p ∨ q`.
%% 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))).
equivalent(A,B) :- prove(A,B), prove(B,A).
```
%% Cell type:code id:f552a71e tags:
``` prolog
?- prove(and(p,q),or(p,q)).
```
%% Output
%% Cell type:code id:f8aca8b7 tags:
``` prolog
?- equivalent(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:markdown id:870939fa tags:
## Some Puzzles
We can return to our Knights & Knave puzzle from the first lecture.
There is an island populated by only knights and knaves.
Knights always say the truth and knaves always lie.
We encounter three persons A,B,C on this island:
- 1. A says: “B is a knave oder C is a knave”
- 2. B says: “A is a knight”
%% Cell type:code id:3187bee7 tags:
``` prolog
?- sat(and(equiv(a,or(not(b),not(c))),equiv(b,a)),I).
```
%% Output
%% Cell type:markdown id:575d68a0 tags:
We can also prove that this is the only solution, i.e., our puzzle implies that A and B are knights and C is a knave:
%% Cell type:code id:df153b0a tags:
``` prolog
?- prove(and(equiv(a,or(not(b),not(c))),equiv(b,a)), and(a,and(b,not(c)))).
```
%% Output
%% Cell type:markdown id:c0299ea9 tags:
Let us now model another puzzle from Raymond Smullyan.
- The King says: One note tells the truth and one does not
- Note on Door 1: This cell contains a princess and there is a tiger in the other cell
- Note on Door 2: One of the cells contains a princess and the other one contains a tiger.
%% Cell type:code id:4363c114 tags:
``` prolog
?- sat(and(equiv(z1,not(z2)),and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))),I).
```
%% Output
%% Cell type:code id:0919b40c tags:
``` prolog
jupyter:retry.
```
%% Output
%% Cell type:markdown id:35fba4c7 tags:
### Appendix: Generating equivalent formulas
%% Cell type:markdown id:78beaf88 tags:
The code below can be used to generate formulas in Prolog using a technique similar to iterative deepening.
We will study this technique much later in the course in the lectures on search.
All you need to know is that generate_formula generates formulas from smaller to deeper formulas.
%% Cell type:code id:51d5630b tags:
``` prolog
generate_formula(X) :-
peano(MaxDepth), gen(X,MaxDepth).
peano(0).
peano(s(X)) :- peano(X).
proposition(p).
proposition(q).
proposition(r).
gen(X,_) :- proposition(X).
gen(and(A,B),s(MaxDepth)) :- gen(A,MaxDepth), gen(B,MaxDepth).
gen(or(A,B),s(MaxDepth)) :- gen(A,MaxDepth), gen(B,MaxDepth).
gen(implies(A,B),s(MaxDepth)) :- gen(A,MaxDepth), gen(B,MaxDepth).
gen(equiv(A,B),s(MaxDepth)) :- gen(A,MaxDepth), gen(B,MaxDepth).
gen(not(A),s(MaxDepth)) :- gen(A,MaxDepth).
```
%% Cell type:code id:f843534d tags:
``` prolog
?-generate_formula(X).
```
%% Output
%% Cell type:code id:3e0e951d tags:
``` prolog
jupyter:retry.
```
%% Output
%% Cell type:code id:8199e19a tags:
``` prolog
jupyter:retry.
```
%% Output
%% Cell type:markdown id:cd56c6d2 tags:
We can now use this together with our other Prolog predicates to generate equivalent formulas:
%% Cell type:code id:fae03e15 tags:
``` prolog
?- generate_formula(Formula), equivalent(and(p,q),Formula), Formula \= and(p,q).
```
%% Output
%% Cell type:code id:94b16168 tags:
``` prolog
jupyter:retry.
```
%% Output
%% Cell type:code id:a49ecd78 tags:
``` prolog
?- generate_formula(Formula), equivalent(and(p,p),Formula).
```
%% Output
%% Cell type:code id:49caff90 tags:
``` prolog
?- generate_formula(Formula), equivalent(and(p,or(p,q)),Formula).
```
%% Output
%% Cell type:markdown id:c57cbe05 tags:
Another side note: we can use the $Var feature of Jupyter Prolog to combine the parser and the show_graph feature:
%% Cell type:code id:c1766e98 tags:
``` prolog
?- parse_wff("(p∧(q∨(¬p)))",Formula).
```
%% Output
%% Cell type:code id:0fd61d87 tags:
``` prolog
jupyter:show_graph(subnode_val(_,_,$Formula,[p/true,q/true]),subtree/3).
```
%% Output
%% Cell type:code id:78693e86 tags:
``` prolog
```
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment