12-April-2006

General format of SPASS output

- input clauses

- reduced clauses

- clauses selected by the "given clause" algorithm

(usable clauses are successively processed and marked as worked off.

If the set of usable clauses is empty, a completion has been found)

- proof

Format of clauses

Clause[split level]justification.literal number

(the split level denotes a specific branch in a tableaux proof)

* literal is maximal in the ordering

** ... and additionally it is an equation, oriented from left to right

+ (negative) literal has been selected

MPI:

- cache CNF computations for optimized skolemization

(workaround until this is fixed: disable optimized skolemization)

- allow U as predicate name

- CNF translation shuold output info

about relation between input axioms and clauses

- treatment of sorted equations

- does it help to mark theorems (that follow from the rest)?

- send SPASS 2.7

Bremen:

- adapt CASL2SPASS translation

- exists! x. phi(x) should become

(exists x. phi(x)) /\ (forall x,y . phi(x) /\ phi(y) => x=y)

done

- in case of a conjunctive goal, send conjuncts individually

A proof of a toplevel conjunction is easier if the conjunction is

split into its conjuncts and each conjunct is proved separately; this

can be implemented in Hets, but the housekeeping is difficult and the

proof reconstruction is difficult.

What to do with proofs of individual conjuncts?

- eliminate user defined equality predicates

- eliminate (some?) subsort definitions, like in RCCDagstuhl.het

- if there is only one sort, eliminate it

- send interesting example with a modular theory -> RCCDagstuhl.het

-> could be saturated per module

-> research paper

- send example with a finite sort -> RCC5.het

translate sort generation constraints with constants only

to a first-order disjunction

- send example with a single sort -> RCCDagstuhl2.het

- send ontology example (DOLCE)