SPASS-communications revision 90450a246c1dcd10734986786cc035c445ae2447
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
90450a246c1dcd10734986786cc035c445ae2447Klaus LuettichA proof of a toplevel conjunction is easier if the conjunction is
90450a246c1dcd10734986786cc035c445ae2447Klaus Luettichsplit into its conjuncts and each conjunct is proved separately; this
90450a246c1dcd10734986786cc035c445ae2447Klaus Luettichcan be implemented in Hets, but the housekeeping is difficult and the
90450a246c1dcd10734986786cc035c445ae2447Klaus Luettichproof reconstruction is difficult.
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
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski - eliminate user defined equality predicates
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski - eliminate (some?) subsort definitions, like in RRCDagstuhl.het
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski - if there is only one sort, eliminate it
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- send interesting example with a modular theory
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski -> could be saturated per module
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski -> research paper
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- send example with a finite sort
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- send example with a single sort (e.g. optimized RCCDagsthul)
cda9a6c85e763522ac4ea19ac566d0d9566ed13bTill Mossakowski- send ontology example (DOLCE)