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"))).
  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").
         ?- example 3 P, eval ("b"::nil) ("a"::nil) P TTorFF.
         TTorFF = ff,
         P = and (p "a") (p "b").
  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