Example script for sheet 2 exercise 2

File contents

; encoding of the formula ((P -> Q) /\ (Q -> R)) -> (P -> R) in smtlib2

; this option is necessary for the get-model and get-valuation commands
(set-option :produce-models true)

; right now, for us any logic suffices because we only need pure propositional logic
; we choose the fragment of first-order logic with uninterpreted functions and
; without quantifiers 
(set-logic QF_UF)

; every non-logical symbol has to be declared, non-quantified variables are modelled as 
; constants which are modelled as nullary functions
; so propositional variables can be modelled as nullary boolean functions 
; (predicates are modelled by boolean functions)
(declare-fun P () Bool)
(declare-fun Q () Bool)
(declare-fun R () Bool)

; save current state on a stack; we will backtrack to here later
(push 1)

; implication is symbolized by "=>", biimplication/equivalence by "=",
; "and", "or" and "not" are written out, 
; everything is written prefix-style
(assert (=> (and (=> P Q) (=> Q R)) (=> P R)))

; check whether all assertions that have been made until now are satisfiable in conjunction
(check-sat)

; if check-sat was succesful, we can retrieve the values of the fulfilling valuation which
; has been discovered
(get-value (P Q R))

; the above example shows that "(P -> Q) /\ (Q -> R) -> (P -> R)" is satisfiable.
; if we want to check for validity, we have to negate it.

; restore state from above
(pop 1)

; assert the negated formula to check for validity
(assert (not (=> (and (=> P Q) (=> Q R)) (=> P R))))

; check satisfiability
(check-sat)

; unsat means unsatisfiable --> the formula was valid.