SPASS-communications revision 4611f3fd020e07a26864895f6bc9ca67925cbcb7
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill MossakowskiGeneral format of SPASS output
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- input clauses
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- reduced clauses
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- clauses selected by the "given clause" algorithm
90450a246c1dcd10734986786cc035c445ae2447Klaus Luettich (usable clauses are successively processed and marked as worked off.
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski If the set of usable clauses is empty, a completion has been found)
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill MossakowskiFormat of clauses
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill MossakowskiClause[split level]justification.literal number
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski(the split level denotes a specific branch in a tableaux proof)
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski* literal is maximal in the ordering
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski** ... and additionally it is an equation, oriented from left to right
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski+ (negative) literal has been selected
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- cache CNF computations for optimized skolemization
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski (workaround until this is fixed: disable optimized skolemization)
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- allow U as predicate name
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- CNF translation shuold output info
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski about relation between input axioms and clauses
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- treatment of sorted equations
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- does it help to mark theorems (that follow from the rest)?
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- send SPASS 2.7
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- adapt CASL2SPASS translation
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski - exists! x. phi(x) should become
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski (exists x. phi(x)) /\ (forall x,y . phi(x) /\ phi(y) => x=y)
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski - in case of a conjunctive goal, send conjuncts individually
7c8efa210ca4b35576481afbddf4f1c7485799efTill Mossakowski A proof of a toplevel conjunction is easier if the conjunction is
7c8efa210ca4b35576481afbddf4f1c7485799efTill Mossakowski split into its conjuncts and each conjunct is proved separately; this
7c8efa210ca4b35576481afbddf4f1c7485799efTill Mossakowski can be implemented in Hets, but the housekeeping is difficult and the
7c8efa210ca4b35576481afbddf4f1c7485799efTill Mossakowski proof reconstruction is difficult.
7c8efa210ca4b35576481afbddf4f1c7485799efTill Mossakowski What to do with proofs of individual conjuncts?
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski - eliminate user defined equality predicates
7c8efa210ca4b35576481afbddf4f1c7485799efTill Mossakowski - eliminate (some?) subsort definitions, like in RCCDagstuhl.het
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski - if there is only one sort, eliminate it
7c8efa210ca4b35576481afbddf4f1c7485799efTill Mossakowski- send interesting example with a modular theory -> RCCDagstuhl.het
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski -> could be saturated per module
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski -> research paper
7c8efa210ca4b35576481afbddf4f1c7485799efTill Mossakowski- send example with a finite sort -> RCC5.het
7c8efa210ca4b35576481afbddf4f1c7485799efTill Mossakowski translate sort generation constraints with constants only
7c8efa210ca4b35576481afbddf4f1c7485799efTill Mossakowski to a first-order disjunction
7c8efa210ca4b35576481afbddf4f1c7485799efTill Mossakowski- send example with a single sort -> RCCDagstuhl2.het
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- send ontology example (DOLCE)
4611f3fd020e07a26864895f6bc9ca67925cbcb7Klaus LuettichQuestions for next meeting:
4611f3fd020e07a26864895f6bc9ca67925cbcb7Klaus Luettich - does "implied" make any difference versus "implies"?