TU Wien:Einführung in wissensbasierte Systeme VU (Egly)/Mandatory Entry Test WS2021

Correct and Incorrect statements:

Correct Statements

Statement	Explanation
Only satisfiable formulas are valid.	A formula is valid if it's true for all possible values of it's terms. A formula is satisfiable if it's true for atleast one value combination for its terms.
A formula is valid iff its negation is unsatisfiable.	If the negation is satisfiable, the formula isn't valid since there exists atleast one combination of values for it's term for which it's not valid.
Satisfiability of a propositional formula can be established using truth table.	A truth table can be built to test every possible value for the terms and hence find atleast one that satisfies the formula.
TC1 is complete. That means, for every unsatisfiable formula there is a closed tableau.	Continuous application of the TC1 rules will always lead to branches with contradiction and hence closed branches. So it is complete.

Incorrect Statements

Statement	Explanation
Some formulas are both valid and unsatisfiable.	If a formula is valid it must be satisfiable, since all values for terms are satisfying the formula.
If a propositional formula is satisfiable, then there can be no counter example to it.	Satisfiable means atleast one model (values for terms that satisfy a formula) exist, so a counter example can still exist. (If the formula was valid, there wouldn't be any conter example possible.)
If a propositional formula is satisfiable, then its negation is unsatisfiable.	Same as statement above. Satisfiable means there exists one model, but countermodels may still exist. Satisfiable is not validity.
A formula is not valid iff it has no model.	A formula is valid if it has only models. A formula can be not valid and have a model, see satisfiable.
There exist propositional formulas which are neither satisfiable nor unsatisfiable.	Propositional logic only deals with propositions which are either true or false. Hence every formula is either satisfiable (has a model) or unsatisfiable (has no model).
TC1 is a calculus for satisfiability in first-order logic, i.e., if a formula is satisfiable, then we can find a closed tableau for it in TC1; if it is unsatisfiable, we cannot find one.	TC1 only closes if a formula is unsatisfiable. If no contradiction is found in a branch, the branch may expand indefinitely.
TC1 is complete. That means that TC1 always terminate.	See statement above. Satisfiable formulas may expand forever and not terminate at all.

Logical Formulas:

Formulas

Tautology?	Formula	Explanation
✅ Yes	(¬s ∨ p) → (s → p)	(¬s ∨ p) = (s → p) Formula becomes: (s → p) → (s → p) which is trivially true
✅ Yes	(p → (q → r)) → ((p → q) → (p → r))	The first term can be expanded and becomes the second term. A implies A is trivially true again.
✅ Yes	p → (q → p)	p q q → p p → (q → p) F F T T T F T T F T F T T T T T
❌ No	p → (p & (q ∨ s))	(q v s) is false if q and s are false, making (p & (q v s)) false even when p is true. This means that the outer implication is false when p is true, but q and s are false.

Sigma Terms

Let Σ = (Func, Pred) be a signature with Func = {f/1,g/2,a/0,b/0} and Pred = {p/1}. Which of the following are terms over Σ? The variables are {x,y,z,...}

Correct / Incorrect	Term / Formula	Reason
✅ Correct	g(f(a),f(b))
✅ Correct	g(f(x),a)
✅ Correct	g(x,f(f(b)))
❌ Incorrect	g(p(b),a)	p is a predicate and cannot be used in a function context.
❌ Incorrect	p(x)	Predicate of variable is a formula, not a term.
❌ Incorrect	f(g(x),y)	f takes only one argument (f/1)
❌ Incorrect	p(g(a,b))	Predicate application creates a formula, not a term.
❌ Incorrect	f(p(x))	p is a predicate and cannot be used in a function context.

Let Σ = (Func, Pred) be a signature with Func = {f/1,g/2,a/0,b/0} and Pred = {p/1,q/2}. The variables are {x,y,z,...}. Which of the following are formulars over Σ?

Correct / Incorrect	Term / Formula	Reason
✅ Correct	p(a) ∨ p(b)
✅ Correct	∀x q(f(f(f(a))),g(b,x))
❌ Incorrect	q(p(x),f(b))
❌ Incorrect	∃x (p(q(x,b)) -> p(a))
❌ Incorrect	p(p(a)) -> q(a,b)
❌ Incorrect	∀x g(x,b)	No predicate application. All quantor requires a predicate.