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

add another cell 


Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent a44371da
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
logic_programming/3_PropositionalLogic.ipynb
+ 47
− 2
View file @ d1215d17
%% 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, ")".
```
%% Output
%% 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: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), ")".
```
%% Output
%% 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).
```
%% Output
%% 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`.
%% Cell type:code id:350b9756 tags:
``` prolog
not(true,false).
not(false,true).
and(true,V,V) :- truth_value(V).
and(false,_,false).
or(true,_,true).
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).
```
%% Output
%% 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:code id:175c00d0 tags:
``` prolog
value(X,Interpretation,Value) :-
atomic(X), % we could also use: proposition(X),
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).
```
%% Output
%% Cell type:code id:eee17774 tags:
``` prolog
?- value(and(p,or(q,not(p))), [p/true, q/false],Res).
```
%% Output
%% 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: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).
```
%% Output
%% 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:code id:23775624 tags:
``` prolog
```
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment