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