Institut für
Informatik, Universität Freiburg
Problem with Exercise 4.2: So, I was translating the relations to clausal form, and it was suddenly pointed out that the resulting clause set would not be Horn.
The Proposition on lecture slide 5 (Satisfiability over Partial Orders) makes a claim only about the satisfiability of pi(Theta) U ORD when pi(Theta) is Horn.
However, this proposition is Proposition 3 from B. Nebel, H.-J. Bürckert, Reasoning about Temporal Relations: A Maximal Tractable Subclass of Allen's Interval Algebra, Journal of the ACM, 42(1):43-66, 1995. (Available as ftp://ftp.informatik.uni-freiburg.de/documents/papers/ki/nebel-burckert-jacm95.ps.gz), and was only incidentally stated for the Horn class only, because the purpose of the discussion of the Proposition and pi(Theta) was to show that the problems can be solved in polynomial time by using unit resolution (which is complete only for Horn theories.) Proposition 3 does not restrict to Horn clauses.
So, yes, the students were right in that based on the lecture and the exercise statement, they could not know that deriving an inconsistency with resolution would really show the unsatisfiability of the interval calculus expressions.
However, I asked in the exercise to apply resolution to showing that pi(Theta) U ORD is unsatisfiable, and this can be done, and is correct as shown by Proposition 3 from Nebel and Bürckert's article. (Irrespective of whether the person doing this knows whether it is correct or not. :-) )
OK, I admit (= it is obvious) that it is more educational to solve the exercises knowing that the solution techniques needed for the exercise are correct.
(s V t)&(s -> p)&(t -> p)&(p <-> q)&(a -> -q)&(b -> -q)&(a V b)
An example input to Otter is the following.
set(auto). formula_list(usable). all x (Jamaican(x) -> -European(x)). all x (Italian(x) -> European(x)). all x (-German(x) -> -(x=gerhard)). exists x (Jamaican(x)). % To show as a refutation proof that there is at least one non-Italian, % we negate it. -(exists x (-Italian(x))). end_of_list.
Why is unsound inference in general useful? (Think about an intelligent robot, or a person, in the real world.) Why would restricting to sound inferences only be a very bad idea? Which inferences you usually do in your everyday life are logically sound?
Solution:
Logical inference (whether a formula is a logical consequence) is used
for deriving things that must hold.
In configuration and planning tasks there are typically several
configurations or plans that fulfill all the given constraints, and
therefore typically none of the solutions are logical consequences of
the constraints. These solutions can be found by identifying models
of the set of constraints.
A special case in which model-finding and logical inference lead to
the same results is when there is exactly one solution.
By model-finding we get an assignment of truth-values to the
propositions (e.g. A = true, B = true, C = false, D = true, E = false, ...)
that satisfies our constraints X,
and by testing logical consequence by some (sound and complete)
inference method for every atomic proposition and its negation separately,
we see that A, B, -C, D and -E are logical consequences of X.