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

add precedence text 


Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent d1215d17
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
logic_programming/3_PropositionalLogic.ipynb
+ 70
− 739
View file @ de95161a
%% Cell type:markdown id:9eb5530a tags: %% Cell type:markdown id:9eb5530a tags:
# Propositional Logic # Propositional Logic
Syntax and Semantics Explained using a Prolog Implementation Syntax and Semantics Explained using a Prolog Implementation
%% Cell type:markdown id:dba70591 tags: %% Cell type:markdown id:dba70591 tags:
## Well-Formed Formulas (WFF) ## Well-Formed Formulas (WFF)
All atomic propositions are WFF) All atomic propositions are WFF)
If a und b are WFF then so are: If a und b are WFF then so are:
- (¬ a) - (¬ a)
- (a ∧ b) - (a ∧ b)
- (a ∨ b) - (a ∨ b)
- (a ⇒ b) - (a ⇒ b)
- (a ⟺ b) - (a ⟺ b)
No other formulas are WFF. No other formulas are WFF.
Comment: a, b are metavariablens outside the syntax of propositional logic. Comment: a, b are metavariablens outside the syntax of propositional logic.
%% Cell type:markdown id:dd01f86a tags: %% Cell type:markdown id:dd01f86a tags:
Maybe this reminds you of formal grammars from a theoretical computer science lecture. 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. 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. 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: 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: %% Cell type:code id:964ebd52 tags:
``` prolog ``` prolog
:- set_prolog_flag(double_quotes, codes). :- set_prolog_flag(double_quotes, codes).
wff --> "p". % atomic proposition wff --> "p". % atomic proposition
wff --> "q". % atomic proposition wff --> "q". % atomic proposition
wff --> "(¬",wff,")". wff --> "(¬",wff,")".
wff --> "(", wff, "∧", wff, ")". wff --> "(", wff, "∧", wff, ")".
wff --> "(", wff, "∨", wff, ")". wff --> "(", wff, "∨", wff, ")".
wff --> "(", wff, "⇒", wff, ")". wff --> "(", wff, "⇒", wff, ")".
wff --> "(", wff, "⟺", wff, ")". wff --> "(", wff, "⟺", wff, ")".
``` ```
%% Output %% Output
%% Cell type:code id:fc6823ad tags: %% Cell type:code id:fc6823ad tags:
``` prolog ``` prolog
?- wff("p",""). ?- wff("p","").
``` ```
%% Output %% Output
%% Cell type:code id:152289b6 tags: %% Cell type:code id:152289b6 tags:
``` prolog ``` prolog
?- wff("(¬p)",""). ?- wff("(¬p)","").
``` ```
%% Output %% Output
%% Cell type:code id:2c3dd1bf tags: %% Cell type:code id:2c3dd1bf tags:
``` prolog ``` prolog
?- wff("(p∧(q∨(¬p)))",""). ?- wff("(p∧(q∨(¬p)))","").
%comment. %comment.
``` ```
%% Output %% 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: %% 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 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: a Prolog term representing the logical formal in the form of a syntax tree:
%% Cell type:code id:78163b60 tags: %% Cell type:code id:78163b60 tags:
``` prolog ``` prolog
:- set_prolog_flag(double_quotes, codes). :- set_prolog_flag(double_quotes, codes).
wff(p) --> "p". % atomic proposition wff(p) --> "p". % atomic proposition
wff(q) --> "q". % atomic proposition wff(q) --> "q". % atomic proposition
wff(not(A)) --> "(¬",wff(A),")". wff(not(A)) --> "(¬",wff(A),")".
wff(and(A,B)) --> "(", wff(A), "∧", wff(B), ")". wff(and(A,B)) --> "(", wff(A), "∧", wff(B), ")".
wff(or(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), ")". wff(equiv(A,B)) --> "(", wff(A), "⟺", wff(B), ")".
``` ```
%% Output
%% Cell type:code id:8ddb568d tags: %% Cell type:code id:8ddb568d tags:
``` prolog ``` prolog
?- wff(Formula,"(¬p)",""). ?- wff(Formula,"(¬p)","").
``` ```
%% Output %% Output
%% Cell type:code id:075dc3b2 tags: %% Cell type:code id:075dc3b2 tags:
``` prolog ``` prolog
?- wff(Formula,"(¬(p∧q))",""). ?- wff(Formula,"(¬(p∧q))","").
``` ```
%% Output %% Output
%% Cell type:code id:338cb7dd tags: %% Cell type:code id:338cb7dd tags:
``` prolog ``` prolog
?- wff(Formula,"(p∧(q∨(¬p)))",""). ?- wff(Formula,"(p∧(q∨(¬p)))","").
``` ```
%% Output %% Output
%% Cell type:markdown id:f9005519 tags: %% Cell type:markdown id:f9005519 tags:
The above Prolog term `and(p,or(q,not(p)))` represents the logical formula in tree form. 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 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): (in future the Jupyter kernel will probably have a dedicated command to show a term graphically):
%% Cell type:code id:f6116612 tags: %% Cell type:code id:f6116612 tags:
``` prolog ``` prolog
subtree(Term,Nr,SubTerm) :- subtree(Term,Nr,SubTerm) :-
Term =.. [_|ArgList], %obtain arguments of the term Term =.. [_|ArgList], %obtain arguments of the term
nth1(Nr,ArgList,SubTerm). % get sub-argument and its position number nth1(Nr,ArgList,SubTerm). % get sub-argument and its position number
% recursive and transitive closure of subtree % recursive and transitive closure of subtree
rec_subtree(Term,Sub) :- Term = Sub. rec_subtree(Term,Sub) :- Term = Sub.
rec_subtree(Term,Sub) :- subtree(Term,_,X), rec_subtree(X,Sub). rec_subtree(Term,Sub) :- subtree(Term,_,X), rec_subtree(X,Sub).
subnode(Sub,[shape/S, label/F],Formula) :- subnode(Sub,[shape/S, label/F],Formula) :-
rec_subtree(Formula,Sub), % any sub-formula Sub of Formula is a node in the graphical rendering 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). functor(Sub,F,_), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect).
``` ```
%% Output
%% Cell type:code id:d7e68593 tags: %% Cell type:code id:d7e68593 tags:
``` prolog ``` prolog
jupyter:print_table(subnode(Node,Dot,and(p,or(q,not(p))))) jupyter:print_table(subnode(Node,Dot,and(p,or(q,not(p)))))
``` ```
%% Output %% Output
Node | Dot | Node | Dot |
:- | :- | :- | :- |
and(p,or(q,not(p))) | [shape/rect,label/and] | and(p,or(q,not(p))) | [shape/rect,label/and] |
p | [shape/egg,label/p] | p | [shape/egg,label/p] |
or(q,not(p)) | [shape/rect,label/or] | or(q,not(p)) | [shape/rect,label/or] |
q | [shape/egg,label/q] | q | [shape/egg,label/q] |
not(p) | [shape/rect,label/not] | not(p) | [shape/rect,label/not] |
p | [shape/egg,label/p] | p | [shape/egg,label/p] |
%% Cell type:code id:3646e3ee tags: %% Cell type:code id:3646e3ee tags:
``` prolog ``` prolog
jupyter:show_graph(subnode(_,_,and(p,or(q,not(p)))),subtree/3) jupyter:show_graph(subnode(_,_,and(p,or(q,not(p)))),subtree/3)
``` ```
%% Output %% Output
%% Cell type:markdown id:11b3a8ad tags: %% Cell type:markdown id:11b3a8ad tags:
Below we will study how one can assign a truth-value to logical formulas like the one above. Below we will study how one can assign a truth-value to logical formulas like the one above.
## Truth tables ## Truth tables
Every logical connective has a truth-table, indicating how it maps the truth of its arguments to its own truth value. 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`. For example, `and` maps inputs `true` and `false` to `false`.
%% Cell type:code id:350b9756 tags: %% Cell type:code id:350b9756 tags:
``` prolog ``` prolog
not(true,false). not(true,false).
not(false,true). not(false,true).
and(true,V,V) :- truth_value(V). and(true,V,V) :- truth_value(V).
and(false,_,false). and(false,_,false).
or(true,_,true). or(true,_,true).
or(false,V,V) :- truth_value(V). or(false,V,V) :- truth_value(V).
implies(A,B,Res) :- not(A,NotA), or(NotA,B,Res). 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). equiv(A,B,Res) :- implies(A,B,AiB), implies(B,A,BiA), and(AiB,BiA,Res).
truth_value(true). truth_value(true).
truth_value(false). truth_value(false).
truth_table(A,B,NotA,AandB,AorB,AiB,AeB) :- truth_table(A,B,NotA,AandB,AorB,AiB,AeB) :-
truth_value(A), truth_value(B), truth_value(A), truth_value(B),
not(A,NotA), and(A,B,AandB), or(A,B,AorB), not(A,NotA), and(A,B,AandB), or(A,B,AorB),
implies(A,B,AiB), equiv(A,B,AeB). implies(A,B,AiB), equiv(A,B,AeB).
``` ```
%% Output
%% Cell type:code id:54b57ff8 tags: %% Cell type:code id:54b57ff8 tags:
``` prolog ``` prolog
jupyter:print_table(truth_table(A,B,NotA,AandB,AorB,AimpliesB,AequivB)) jupyter:print_table(truth_table(A,B,NotA,AandB,AorB,AimpliesB,AequivB))
``` ```
%% Output %% Output
A | B | NotA | AandB | AorB | AimpliesB | AequivB | A | B | NotA | AandB | AorB | AimpliesB | AequivB |
:- | :- | :- | :- | :- | :- | :- | :- | :- | :- | :- | :- | :- | :- |
true | true | false | true | true | true | true | true | true | false | true | true | true | true |
true | false | false | false | true | false | false | true | false | false | false | true | false | false |
false | true | true | false | true | true | false | false | true | true | false | true | true | false |
false | false | true | false | false | true | true | false | false | true | false | false | true | true |
%% Cell type:code id:175c00d0 tags: %% Cell type:code id:175c00d0 tags:
``` prolog ``` prolog
value(X,Interpretation,Value) :- value(X,Interpretation,Value) :-
atomic(X), % we could also use: proposition(X), atomic(X), % we could also use: proposition(X),
member(X/Value,Interpretation). member(X/Value,Interpretation).
value(and(A,B),I,Val) :- value(A,I,VA), value(B,I,VB), value(and(A,B),I,Val) :- value(A,I,VA), value(B,I,VB),
and(VA,VB,Val). and(VA,VB,Val).
value(or(A,B),I,Val) :- value(A,I,VA), value(B,I,VB), value(or(A,B),I,Val) :- value(A,I,VA), value(B,I,VB),
or(VA,VB,Val). or(VA,VB,Val).
value(not(A),I,Val) :- value(A,I,VA), value(not(A),I,Val) :- value(A,I,VA),
not(VA,Val). not(VA,Val).
value(implies(A,B),I,Val) :- value(or(not(A),B),I,Val). value(implies(A,B),I,Val) :- value(or(not(A),B),I,Val).
value(equiv(A,B),I,Val) :- value(equiv(A,B),I,Val) :-
value(and(implies(A,B),implies(B,A)),I,Val). value(and(implies(A,B),implies(B,A)),I,Val).
``` ```
%% Output
%% Cell type:code id:eee17774 tags: %% Cell type:code id:eee17774 tags:
``` prolog ``` prolog
?- value(and(p,or(q,not(p))), [p/true, q/false],Res). ?- value(and(p,or(q,not(p))), [p/true, q/false],Res).
``` ```
%% Output %% Output
%% Cell type:code id:78473da0 tags: %% Cell type:code id:78473da0 tags:
``` prolog ``` prolog
jupyter:print_table(value(and(p,or(q,not(p))), [p/P, q/Q],Res)) jupyter:print_table(value(and(p,or(q,not(p))), [p/P, q/Q],Res))
``` ```
%% Output %% Output
P | Q | Res | P | Q | Res |
:- | :- | :- | :- | :- | :- |
true | true | true | true | true | true |
true | false | false | true | false | false |
false | true | false | false | true | false |
false | false | false | false | false | false |
%% Cell type:code id:2ee60c15 tags: %% Cell type:code id:2ee60c15 tags:
``` prolog ``` prolog
subnode_val(Sub,[shape/S, label/F, style/filled, fillcolor/C],Formula,Interpretation) :- 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 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), functor(Sub,F,_), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect),
(value(Sub,Interpretation,true) -> C=olive ; C=sienna1). (value(Sub,Interpretation,true) -> C=olive ; C=sienna1).
``` ```
%% Output
%% Cell type:code id:2b497dad tags: %% Cell type:code id:2b497dad tags:
``` prolog ``` prolog
jupyter:show_graph(subnode_val(_,_,and(p,or(q,not(p))),[p/true,q/false]),subtree/3) jupyter:show_graph(subnode_val(_,_,and(p,or(q,not(p))),[p/true,q/false]),subtree/3)
``` ```
%% Output %% Output
%% Cell type:code id:0fd23f05 tags: %% Cell type:code id:0fd23f05 tags:
``` prolog ``` prolog
jupyter:show_graph(subnode_val(_,_,and(p,or(q,not(p))),[p/true,q/true]),subtree/3) jupyter:show_graph(subnode_val(_,_,and(p,or(q,not(p))),[p/true,q/true]),subtree/3)
``` ```
%% Output %% Output
%% Cell type:code id:23775624 tags: %% Cell type:code id:23775624 tags:
``` prolog ``` prolog
?- use_module(library(clpfd)).
```
%% Output
%% Cell type:code id:7a6e29ed tags:
``` prolog
``` ```
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment