# CSE 360 Homework 4

This assignment concerns one problem: how to determine whether or not a formula of propositional logic is a tautology (in classical logic). We shall attempt to do a straightforward specification of truth table evaluation.

Propositional formulas will be coded up as follows.

```kind bool  type.
type tt    bool.		 % true
type ff    bool.		 % false
type neg   bool -> bool.	 % negation
type and   bool -> bool -> bool. % conjunction
type or    bool -> bool -> bool. % disjunction
type imp   bool -> bool -> bool. % implications
type p     string -> bool.	 % build propositional constants

type example    int -> bool -> o.

example 1 (or (p "a") (neg (p "a"))).
example 2 (neg (neg (or (p "a") (neg (p "a"))))).
example 3 (and (p "a") (p "b")).
example 4 (imp (p "a") (p "b")).
example 5 (imp (imp (and (p "a") (p "b")) (p "c"))
(imp (p "a") (imp (p "b") (p "c")))).
example 6 (imp (imp (and (p "a") (p "b")) (p "c"))
(imp (p "a") (imp (p "b") (p "d")))).
```
To solve this problem, write the following predicates.
1. Given a propositional formula, we need to collect together all of the propositional letters that appear in it. So, write a specification of the following predicate.
```type collect   bool -> list string -> o.
```
An example of using this predicate is
```?- example 6 P, collect P L.

L = "c" :: "a" :: "b" :: "d" :: nil,
P = imp (imp (and (p "a") (p "b")) (p "c"))
(imp (p "a") (imp (p "b") (p "d"))).

yes
?-
```
2. Next, we will need to assign to the propositional connectives true and false values. This can be done using a predicate that divides a list into two disjoint lists. Thus, write a predicate
```     type divide_list    list A -> list A -> list A -> o.
```
such that (divide_list L TS TS) is provable if and only if the list L can be split into TS and FS. In general, there are 2^n ways to split a list of n members. For example,
```     ?- divide_list ("a"::"b"::"c"::nil) TS FS.

FS = "a" :: "b" :: "c" :: nil,
TS = nil.
;

FS = "b" :: "c" :: nil,
TS = "a" :: nil.
;

FS = "a" :: "c" :: nil,
TS = "b" :: nil.
;

FS = "c" :: nil,
TS = "a" :: "b" :: nil.
;

FS = "a" :: "b" :: nil,
TS = "c" :: nil.
;

FS = "b" :: nil,
TS = "a" :: "c" :: nil.
;

FS = "a" :: nil,
TS = "b" :: "c" :: nil.
;

FS = nil,
TS = "a" :: "b" :: "c" :: nil.
;
no more solutions
?-
```
3. Finally, write a predicate to "evaluation" a propositional formula given that we assume some letters in it are true and some letters in it are false. Specify a predicate
```     type eval  list string -> list string -> bool -> bool -> o.
```
so that (eval TS FS Prop TTorFF) is probable if and only if the value of Prop is TTorFF (which is either tt for true or ff for false). For example,
```     ?- example 3 P, eval ("a"::nil) ("b"::nil) P TTorFF.

TTorFF = ff,
P = and (p "a") (p "b").

yes
?- example 3 P, eval ("b"::nil) ("a"::nil) P TTorFF.

TTorFF = ff,
P = and (p "a") (p "b").

yes
?-
```
4. Finally, write a predicate
```     type  type tautology    bool -> o.
```
that determines whether or not its argument is a tautology. Thus,
```     ?- example N P, tautology P.

P = or (p "a") (neg (p "a")),
N = 1.
;

P = neg (neg (or (p "a") (neg (p "a")))),
N = 2.
;

P = imp (imp (and (p "a") (p "b")) (p "c"))
(imp (p "a") (imp (p "b") (p "c"))),
N = 5.
;
no more solutions
?-
```
Hint: I don't know anyway to do this that does not use negation-as-failure somewhere is this problem.

Lectures / Modules / Homeworks / Syllabus