Description
Programmation fonctionnelle
INFO0054-1
Christophe Debruyne
(c.debruyne@uliege.be)
Some details
β’ Project description on eCampus
β’ Groups of three people
Context: semantic tableau for propositional logics
Semantic Tableaux are a well-known and popular algorithm to decide (decision procedure) weather a set of formulae is satisfiable (has a model, or “can happen”)
In propositional logic, truth tables can become quite large. We have 2! possibilities where π corresponds with the number of propositions π, π, β¦ in used in our set.
Propositional logics: Some background
β’ Given A, a countably infinite set of elements of proposition symbols p, q, r, β¦ which we call the alpha set or atomic formulas.
β’ Given π = π! βͺ π” where
β’ π! = Β¬ the set of unary logical operators
β’ π” = β§,β¨, β the set of binary logical operators
β’ The set of formulas is inductively defined by the following rules:
β’ Any element of A is a formula;
β’ If π is a formula, then Β¬π is a formula;
β’ If π and π are formulas, then π β¨ π , π β§ π , and π β π are formulas;
β’ Nothing else is a formula.
Semantic Tableaux
The result of applying the semantic tableau is a structure containing one or more tableaux. A tableau (“panel”) contains a set of formulas. One can call a tableau of a semantic tableau a branch.
Open vs. Closed tableaux and branches:
β’ A branch/tableau is said to be closed if the branch contains a contradiction, that is: the branch contains both a π and a Β¬π
β’ A branch/tableau is said to be open if all binary operators have been eliminated (i.e., it only contains proposition symbols or their negation) and it does not contain a contradiction.
β’ A semantic tableau is said to be closed if all its tableaux/branches are closed.
β’ A semantic tableau is said to be open if at least one tableau/branch is open.
A set of formulas is called satisfiable if there is at least one model. I.e., at least one mapping of truth values to proposition symbols that make all the formulas in the set true.
Is F = {π β¨ π, π, Β¬π} satisfiable? Start:
π! = {π β¨ π, π, Β¬π}
Is π! closed? No
Does π! contain formulas we can eliminate? Yes: π β¨ π.
The formula π β¨ π is true if π is true (no matter the truth value of π) OR π is true (no matter the truth value of π). The branches thus split. We remove π β¨ π and copy the table. We place π in the original table, and π in the copy.
π! = {π, π, Β¬π}
π” = {π, π, Β¬π}
π! = {π, π, Β¬π}
π” = {π, π, Β¬π}
β’ π!
β’ Is π! closed? No
β’ Does π! contain formulas that can be eliminated? No
β’ π! is therefore open
β’ π”
β’ Is π” closed? Yes
β’ At least one branch is open. π! contains at least one model and the set F = {π β¨ π, π, Β¬π} is therefore satisfiable!
π! = {π, π, Β¬π}
π” = {π, π, Β¬π}
How many models does π! contain and why?
β’ 1, as it assigns a truth value for each proposition symbol πΉ
β’ π£(π) = 1, π£(π) = 0, and π£(π) = 1
Can a branch contain multiple models? Discuss.
Elimination rules
¬¬π is true/false if π is true/false
π β¨ πis true if π is true OR π is true
Β¬ π β¨ π is true if π is false AND π is false
π π π β π
0 0 1
0 1 1
1 0 0
1 1 1
π β§ πis true if π is true AND π is true Β¬ π β§ π is true if π is false OR π is false
π β πis true if π is false OR π is true
Β¬ π β π is true if π is true AND π is false
Logical consequence and tautologies
A formula π is said to be a logical consequence (or valid under) of a set of hypotheses πΉ
β’ If all models of πΉ are also models of π
β’ Or, if πΉ βͺ Β¬π is unsatisfiable!
β’ Why is that? Does this technique remind you of something?
β’ If πΉ βͺ Β¬π is satisfiable, that means we have found counterexamples
β’ A counterexample is a model that makes πΉ true, but π false!
Tautologies and contradictions
A tautology π is a formula that is always true.
β’ In other words, Β¬π is unsatisfiable
A contradiction π is a formula that is always falls
β’ In other words, π is unsatisfiable
Models and counterexamples
Of instance, if F uses the propositions π, π, and π and an open branch only mentions π and Β¬π. Then that branch contains truth values for π and π independent from the proposition π It thus contains two models:
β’ π£! π = 1, π£! π = 0, π£!(π) = 1
β’ π£”(π) = 1, π£”(π) = 0, π£”(π) = 0
The project:
Part 1: the function semtab (40%)
Formulas look as follows:
β’ p
β’ (AND (OR p q) (NOT s))
β’ (IFTHEN p (OR r p))
β’ (NOT (NOT s))
β’ β¦
Given a list of formulas (or other abstract data type), semtab applies the semantic tableau algorithm and returns a data structure that contains the branches.
Ensure your implementation is elegant, efficient, and extensible.
Part 2: the module (30%)
The function semtab provides the basis for all other functions. You are required to implement functions for:
β’ satisfiable? ; is F satisfiable?
β’ valid? ; is a formula f valid under F?
β’ tautology? ; is a formula f a tautology?
β’ contradiction? ; is a formula f a contradiction?
β’ models ; w.r.t. the propositions in F, what are all the models?
β’ counterexamples ; what are all the counterexamples when f is not valid under F?
Specify your functions (and any auxiliary functions). Motivate your approach and chosen data structures.
Part 2: the module (30%)
> (satisfiable? ‘(a (NOT b) (IFTHEN (NOT b) c)))
#t
> (valid? ‘a ‘((OR a (NOT a))))
#f
> (tautology? ‘(OR a (NOT a)))
#t
> (contradiction? ‘(AND a (NOT a)))
#t
> (models ‘(a (NOT b) (IFTHEN (NOT b) c)))
;; Up to you to decide ο
> (counterexamples? ‘a ‘((OR a (NOT a))))
;; Up to you to decide
Part 3: extensions (20%)
1. Conceptualize, formulate and implement elimination rules for
β’ EQUIV
β’ XOR
β’ NAND
β’ XNOR
2. Conceptualize, formalize, and implement a generalized approach for AND and OR with n => 1 arguments
Report (10%)
β’ A small technical report containing
β’ A description and motivation for Parts 1, 2, 3, (and 4)
β’ Describe and motivate the data representations you have chosen
β’ For tableaux and branches
β’ For extensibility and generalized approaches
β’ For efficacy
β’ β¦
β’ Provide examples on how to use your module!
The project:
Part 4: visualization (10% bonus)
β’ Load your semantic tableau module in a new file in which you implement the visualization.
β’ WATCH OUT. Unless you have found an elegant way to represent semantic tableaux, I would urge you to make a copy of the module.
A final example!
β’ Is π β π β π valid under π β π β π ?
A final example!
β’ T1 contains the counterexamples
β’ π£1(π) = 0, π£1(π) = 0, π£1(π) = 0
β’ T3 contains the counterexamples
β’ π£1(π) = 0, π£1(π) = 0, π£1(π) = 0
β’ π£2(π) = 0, π£2(π) = 1, π£2(π) = 0
β’ T2 contains the counterexamples
β’ π£2(π) = 0, π£2(π) = 1, π£2(π) = 0
We thus have two counterexamples, and T3 contained both.
Semantic tableaux started as panels.
Source: https://www.museodelprado.es/en/the-collection/sxix-painting
Semantic tableaux started as panels. The convenient tree representations (capturing relationships between tableaux) came later.
We now call the whole a semantic tableau. Each node in the tree representation contains a tableau.
The indices 1,2, β¦ are used to disambiguate branches and are not used to indicate order. In fact, one does not have to give “names” to branches and tableaux.
There are various ways to represent (semantic) tableaux and branches. Each with their advantages and disadvantages. ο
Reviews
There are no reviews yet.