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")))).

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.