Exam SS 2019

1) Consider the formula: ((p/\r)-> ~q) \/ ((q <-> r) -> ~p).
a) Which atoms are pure in the above formula?
b) Compute a clausal normal form C of the above formula by applying the CNF transformation algorithm with naming and optimization based on polarities of subformulas.
c) Decide the satisfiability of the computed CNF formula C by applying the DPLL method to C.
If C is satisfiable, give an interpretation which satisfies it.

2) Let A be a propositional formula with n>=1 propositional variables such that: 
		- A is not a propositional atom, and
		- A is built from propositional atoms using only ~ and <->.
How many branches does a splitting tree of A have? Provide a sufficiently detailed explanation of your work.

3) Consider the formula: read(write(A,b,f(b)),a)=f(a+1)/\ f(a) != f(a+1)/\(a=b \/ f(a)=f(b)),
where a,b are constants, f is a unary function symbol, A is an array constant and +,1 are interpreted in the standard way over intergers.
Use the Nelson-Oppen decision procedure for reasoning in the combination of the theories of arrays, uninterpreted functions, and linear integer arithmetic.
Use the decision procedures for the theory of arrays and the theory of uninterpreted functions and use simple mathematical reasoning for deriving new equalities among the constants in the theory of linear integer arithmetic.
If the formula is satisfiable, give an interpretation that satisfies the formula.

4) Consider the KBO ordering > generated by the precedence f >> c >> b >> a and the weight function w with w(f)=0, w(b)=w(c)=1 and w(a)=2.
Let sigma be a well-behaved selection function wrt >. Consider the set S of ground formulas:
		a=f(b)\/b=f(b)
		f(b)=c
		a!=c
		b!=c
Show that S is unsatisfiable by applying saturation on S using an inference process based on the ground superposition  calculus Sup>,sigma.
Give details on what literals are selected and which terms are maximal.

5) Consider the following set S of clauses: x=a, f(b)!=f(c), where f is a function symbol, x is a variable and a,b,c are constants.
Give a refutation of S by using the non-ground superposition system  Sup.
For each newly derived clause, label the clauses from which it was derived by which inference rule and indicate most general unifiers.

6) Let > be a Knuth-Bendix ordering KBO and sigma a well-behaved selection function wrt >.
Consider the following inference instance of the non-ground superposition calculus Sup>,sigma:
		l=r		l'=t\/D
		-------------------------
			(r theta = t)\/D
where l theta = l', l>r, l'>t, r theta > t, (l=r) theta > D, (l'=t) > D and l'=t is selected in l'=t\/D.
a) Is ((r theta = t) \/ D) > (l'=t \/ D)?
b) Does l'=t \/ D always become redundant after the inference is applied?
Justify your answers.