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