UVa CS2120-002 F23 Midterm Exam

Propositional Logic: Syntax, Sematics, Satisfiability

This section of the exam simply includes our formal definition of the syntax and semantics of propositional logic and of functions that determine whether a given expression is valid, satisfiable, or unsatisfiable.

Syntax

-- variables
structure var : Type :=  (n: Nat)

-- connectives/operators
inductive unary_op : Type | not
inductive binary_op : Type
| and
| or
| imp
| iff

-- expressions (abstract syntax)
inductive Expr : Type
| var_exp (v : var)
| un_exp (op : unary_op) (e : Expr)
| bin_exp (op : binary_op) (e1 e2 : Expr)

-- concrete syntax 
notation "{"v"}" => Expr.var_exp v
prefix:max "¬" => Expr.un_exp unary_op.not 
infixr:35 " ∧ " => Expr.bin_exp binary_op.and  
infixr:30 " ∨ " => Expr.bin_exp binary_op.or 
infixr:25 " ⇒ " =>  Expr.bin_exp binary_op.imp
infixr:20 " ⇔ " => Expr.bin_exp binary_op.iff

Semantics

-- meanings of unary operators
def eval_un_op : unary_op → (Bool → Bool)
| unary_op.not => not

-- missing binary Boolean operators
def implies : Bool → Bool → Bool
| true, false => false
| _, _ => true

def iff : Bool → Bool → Bool
| true, true => true
| false, false => true
| _, _ => false

-- meanings of binary operators
def eval_bin_op : binary_op → (Bool → Bool → Bool)
| binary_op.and => and
| binary_op.or => or
| binary_op.imp => implies
| binary_op.iff => iff

-- The interpretation type
def Interp := var → Bool 

-- The meanings of expressions "under" given interpretations
def eval_expr : Expr → Interp → Bool 
| (Expr.var_exp v),        i => i v
| (Expr.un_exp op e),      i => (eval_un_op op) (eval_expr e i)
| (Expr.bin_exp op e1 e2), i => (eval_bin_op op) (eval_expr e1 i) (eval_expr e2 i)

Satisfiability

We built a satisfiability checker for propositional logic, in several pieces. This subsection includes all definitions.

Truth Table Input Rows

-- Nat to Binary
-- You don't need to worry about the "have" part
def right_bit (n : Nat) := n%2
def shift_right (n : Nat) := n/2
def 
nat_to_bin: Nat → List Nat
nat_to_bin
Warning: declaration uses 'sorry'
Warning: declaration uses 'sorry' : 
Nat: Type
Nat → 
List: Type → Type
List 
Nat: Type
Nat
| 
0: Nat
0     => [
0: Nat
0]
| 
1: Nat
1     => [
1: Nat
1]
| 
n': Nat
n' + 2 =>
  have : (
shift_right: Nat → Nat
shift_right (
n': Nat
n' + 
2: Nat
2)) < (
n': Nat
n' + 
2: Nat
2) := 
sorry: shift_right (n' + 2) < n' + 2
sorry
  
nat_to_bin: Nat → List Nat
nat_to_bin (
shift_right: Nat → Nat
shift_right (
n': Nat
n' + 
2: Nat
2)) ++ [
right_bit: Nat → Nat
right_bit (
n': Nat
n' + 
2: Nat
2)]

-- Left pad with zeros
def 
zero_pad: Nat → List Nat → List Nat
zero_pad : 
Nat: Type
Nat → 
List: Type → Type
List 
Nat: Type
Nat → 
List: Type → Type
List 
Nat: Type
Nat
  | 
v: Nat
v, 
l: List Nat
l => 
zero_pad_recursive: Nat → List Nat → List Nat
zero_pad_recursive (
v: Nat
v - (
l: List Nat
l.
length: {α : Type} → List α → Nat
length)) 
l: List Nat
l
where 
zero_pad_recursive: Nat → List Nat → List Nat
zero_pad_recursive : 
Nat: Type
Nat → 
List: Type → Type
List 
Nat: Type
Nat → 
List: Type → Type
List 
Nat: Type
Nat
  | 
0: Nat
0, 
l: List Nat
l => 
l: List Nat
l
  | 
v': Nat
v'+1, 
l: List Nat
l => 
zero_pad_recursive: Nat → List Nat → List Nat
zero_pad_recursive 
v': Nat
v' (
0: Nat
0::
l: List Nat
l)

-- Make row of bits at index "row" padded out to "cols" wide 
def 
mk_bit_row: Nat → Nat → List Nat
mk_bit_row : (
row: Nat
row: 
Nat: Type
Nat) → (
cols: Nat
cols : 
Nat: Type
Nat) → 
List: Type → Type
List 
Nat: Type
Nat
| 
r: Nat
r, 
c: Nat
c => 
zero_pad: Nat → List Nat → List Nat
zero_pad 
c: Nat
c (
nat_to_bin: Nat → List Nat
nat_to_bin 
r: Nat
r)

-- Convert list of bits to list of bools
def 
bit_to_bool: Nat → Bool
bit_to_bool : 
Nat: Type
Nat → 
Bool: Type
Bool
| 
0: Nat
0 => 
false: Bool
false
| _ => 
true: Bool
true

def 
bit_list_to_bool_list: List Nat → List Bool
bit_list_to_bool_list : 
List: Type → Type
List 
Nat: Type
Nat → 
List: Type → Type
List 
Bool: Type
Bool
| [] => 
[]: List Bool
[]
| 
h: Nat
h::
t: List Nat
t => (
bit_to_bool: Nat → Bool
bit_to_bool 
h: Nat
h) :: (
bit_list_to_bool_list: List Nat → List Bool
bit_list_to_bool_list 
t: List Nat
t)

-- Make row'th row of truth table with vars variables
def 
mk_row_bools: Nat → Nat → List Bool
mk_row_bools : (
row: Nat
row : 
Nat: Type
Nat) → (
vars: Nat
vars : 
Nat: Type
Nat) → 
List: Type → Type
List 
Bool: Type
Bool
| 
r: Nat
r, 
v: Nat
v => 
bit_list_to_bool_list: List Nat → List Bool
bit_list_to_bool_list (
mk_bit_row: Nat → Nat → List Nat
mk_bit_row 
r: Nat
r 
v: Nat
v)

Interpretations

-- Convert list of bools to interpretation
def 
override: Interp → var → Bool → Interp
override : 
Interp: Type
Interp → 
var: Type
var → 
Bool: Type
Bool → 
Interp: Type
Interp
| 
old_interp: Interp
old_interp, 
var: _root_.var
var, 
new_val: Bool
new_val => 
  (λ 
v: _root_.var
v => if (
v: _root_.var
v.
n: _root_.var → Nat
n == 
var: _root_.var
var.
n: _root_.var → Nat
n)     -- when applied to var
          then 
new_val: Bool
new_val          -- return new value
          else 
old_interp: Interp
old_interp 
v: _root_.var
v)  -- else retur old value

def 
bools_to_interp: List Bool → Interp
bools_to_interp : 
List: Type → Type
List 
Bool: Type
Bool → 
Interp: Type
Interp
  | 
l: List Bool
l => 
bools_to_interp_helper: Nat → List Bool → Interp
bools_to_interp_helper 
l: List Bool
l.
length: {α : Type} → List α → Nat
length 
l: List Bool
l
where 
bools_to_interp_helper: Nat → List Bool → Interp
bools_to_interp_helper : (
vars: Nat
vars : 
Nat: Type
Nat) → (
vals: List Bool
vals : 
List: Type → Type
List 
Bool: Type
Bool) → 
Interp: Type
Interp
  | _, [] => (λ 
_: var
_ => 
false: Bool
false)
  | 
vars: Nat
vars, 
h: Bool
h::
t: List Bool
t =>
    let 
len: Nat
len := (
h: Bool
h::
t: List Bool
t).
length: {α : Type} → List α → Nat
length
    
override: Interp → var → Bool → Interp
override (
bools_to_interp_helper: Nat → List Bool → Interp
bools_to_interp_helper 
vars: Nat
vars 
t: List Bool
t) (
var.mk: Nat → var
var.mk (
vars: Nat
vars - 
len: Nat
len)) 
h: Bool
h 

-- Make an interpretation for given row with "vars" variables
def 
mk_interp_vars_row: Nat → Nat → Interp
mk_interp_vars_row : (
vars: Nat
vars: 
Nat: Type
Nat) → (
row: Nat
row: 
Nat: Type
Nat) → 
Interp: Type
Interp
| 
v: Nat
v, 
r: Nat
r => 
bools_to_interp: List Bool → Interp
bools_to_interp (
mk_row_bools: Nat → Nat → List Bool
mk_row_bools 
r: Nat
r 
v: Nat
v)

-- Given number of variables, return list of interpretations
def 
mk_interps: Nat → List Interp
mk_interps (
vars: Nat
vars : 
Nat: Type
Nat) : 
List: Type → Type
List 
Interp: Type
Interp := 
  
mk_interps_helper: Nat → Nat → List Interp
mk_interps_helper (
2: Nat
2^
vars: Nat
vars) 
vars: Nat
vars
where 
mk_interps_helper: Nat → Nat → List Interp
mk_interps_helper : (
rows: Nat
rows : 
Nat: Type
Nat) → (
vars: Nat
vars : 
Nat: Type
Nat) → 
List: Type → Type
List 
Interp: Type
Interp
  | 
0: Nat
0, _         => 
[]: List Interp
[]
  | (
n': Nat
n' + 1), 
v: Nat
v  => (
mk_interp_vars_row: Nat → Nat → Interp
mk_interp_vars_row 
v: Nat
v 
n': Nat
n')::
mk_interps_helper: Nat → Nat → List Interp
mk_interps_helper 
n': Nat
n' 
v: Nat
v

-- Count the number of variables in a given expression
def 
max_variable_index: Expr → Nat
max_variable_index : 
Expr: Type
Expr → 
Nat: Type
Nat
| 
Expr.var_exp: var → Expr
Expr.var_exp (
var.mk: Nat → var
var.mk 
i: Nat
i) => 
i: Nat
i
| 
Expr.un_exp: unary_op → Expr → Expr
Expr.un_exp _ 
e: Expr
e => 
max_variable_index: Expr → Nat
max_variable_index 
e: Expr
e
| 
Expr.bin_exp: binary_op → Expr → Expr → Expr
Expr.bin_exp _ 
e1: Expr
e1 
e2: Expr
e2 => 
max: {α : Type} → [self : Max α] → α → α → α
max (
max_variable_index: Expr → Nat
max_variable_index 
e1: Expr
e1) (
max_variable_index: Expr → Nat
max_variable_index 
e2: Expr
e2)

def 
num_vars: Expr → Nat
num_vars : 
Expr: Type
Expr → 
Nat: Type
Nat := λ 
e: Expr
e => 
max_variable_index: Expr → Nat
max_variable_index 
e: Expr
e + 
1: Nat
1

Truth Table Output Column

def 
eval_expr_interps: List Interp → Expr → List Bool
eval_expr_interps : 
List: Type → Type
List 
Interp: Type
Interp → 
Expr: Type
Expr → 
List: Type → Type
List 
Bool: Type
Bool
| [], _ => 
[]: List Bool
[]
| 
h: Interp
h::
t: List Interp
t, 
e: Expr
e => 
eval_expr_interps: List Interp → Expr → List Bool
eval_expr_interps 
t: List Interp
t 
e: Expr
e ++ [
eval_expr: Expr → Interp → Bool
eval_expr 
e: Expr
e 
h: Interp
h]

-- Given expression, return truth table outputs by ascending row index
def 
truth_table_outputs: Expr → List Bool
truth_table_outputs : 
Expr: Type
Expr → 
List: Type → Type
List 
Bool: Type
Bool
| 
e: Expr
e =>  
eval_expr_interps: List Interp → Expr → List Bool
eval_expr_interps (
mk_interps: Nat → List Interp
mk_interps (
num_vars: Expr → Nat
num_vars 
e: Expr
e)) 
e: Expr
e

Satisfiability Checkers

-- functions to check if bool list has any, resp. all, values true
def 
reduce_or: List Bool → Bool
reduce_or : 
List: Type → Type
List 
Bool: Type
Bool → 
Bool: Type
Bool 
| [] => 
false: Bool
false
| 
h: Bool
h::
t: List Bool
t => 
or: Bool → Bool → Bool
or 
h: Bool
h (
reduce_or: List Bool → Bool
reduce_or 
t: List Bool
t)

def 
reduce_and: List Bool → Bool
reduce_and : 
List: Type → Type
List 
Bool: Type
Bool → 
Bool: Type
Bool 
| [] => 
true: Bool
true
| 
h: Bool
h::
t: List Bool
t => 
and: Bool → Bool → Bool
and 
h: Bool
h (
reduce_and: List Bool → Bool
reduce_and 
t: List Bool
t)

-- Three main functions: test given expression for satsfiability properties
def 
is_sat: Expr → Bool
is_sat : 
Expr: Type
Expr → 
Bool: Type
Bool := λ 
e: Expr
e : 
Expr: Type
Expr => 
reduce_or: List Bool → Bool
reduce_or (
truth_table_outputs: Expr → List Bool
truth_table_outputs 
e: Expr
e)
def 
is_valid: Expr → Bool
is_valid : 
Expr: Type
Expr → 
Bool: Type
Bool := λ 
e: Expr
e : 
Expr: Type
Expr => 
reduce_and: List Bool → Bool
reduce_and (
truth_table_outputs: Expr → List Bool
truth_table_outputs 
e: Expr
e)
def 
is_unsat: Expr → Bool
is_unsat : 
Expr: Type
Expr → 
Bool: Type
Bool := λ 
e: Expr
e : 
Expr: Type
Expr => 
not: Bool → Bool
not (
is_sat: Expr → Bool
is_sat 
e: Expr
e)

Quick Demo

-- some atomic/variable expressions
def 
Bread: Expr
Bread  : 
Expr: Type
Expr := {
var.mk: Nat → var
var.mk 
0: Nat
0}
def 
Cheese: Expr
Cheese : 
Expr: Type
Expr := {
var.mk: Nat → var
var.mk 
1: Nat
1}
def 
Jam: Expr
Jam    : 
Expr: Type
Expr := {
var.mk: Nat → var
var.mk 
2: Nat
2}

#eval
true
 
is_sat: Expr → Bool
is_sat (
Bread: Expr
Bread)
#eval
false
 
is_sat: Expr → Bool
is_sat (
Bread: Expr
Bread ∧ ¬
Bread: Expr
Bread)
#eval
false
 
is_valid: Expr → Bool
is_valid (
Bread: Expr
Bread ∧ ¬
Bread: Expr
Bread)
#eval
true
 
is_valid: Expr → Bool
is_valid (
Bread: Expr
Bread ∨ ¬
Bread: Expr
Bread)
#eval
true
 
is_unsat: Expr → Bool
is_unsat (
Bread: Expr
Bread ∧ ¬
Bread: Expr
Bread)