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)
meeting on 2006-07-13:
- does "implied" make any difference versus "implies"?
Ans: no difference
- does "-interactive" works? and how does it work?
Ans: Not documented... One Bug... not supported; no strict timeout possible.
- how are declarations numbered? and how can we trace them back, hence
they are present in the "used formulae"-list?
Ans: -PLabels shows all labels also the genrated ones (-DocProof)
They look into it. They add the possibility to give labels
for declarations.
- how to interpret the models generated by SPASS?
Ans: quotient of Herbrand models with equvalence classes (Word problem)
Satureted clause set
-FPModel=2; clause set; initial model
finite description of the model
Till and Klaus will discuss this and formulate additinal questions
if neccessary.
- What is SPASS doing after displaying the statistics? Sometimes it
needs more than 5 minutes to shut down...
Ans: Problem is known; it is freeing memory needed for debugging only;
they try to solve it.
New interface to SPASS:
- generate Clause Set and relation clause name -> axiom label
- send only clauses depending on selected sentences
=> as quick as -interactive with strict timeout
Bremen:
- send RCCDagstuhl.het in parts
Questions for next meeting: