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.

- 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 ?-

- 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 ?-

- 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 ?-

- 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