; 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) ; 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))