1
@setfilename spassfaq.info
2
@settitle frequently asked questions about SPASS
5
@node spassfaq, , tptp2dfg, Top
10
Q: How can I get an answer substitution?
14
A: There are no meta predicates in SPASS available. Hence,
15
this functionality is not directly supported. However it
16
can be achieved by a trick. The idea is to add a new literal
17
to the conjecture clause that carries the substitution and
18
will definitely be resolved away in the final step of the proof.
19
For example: let x be the variable where we are
20
interested in the subsitution. Let x occur in the single
21
conjecture clause C. Then extend this clause to C,P(x,a,y)
22
and add the clause -P(z,u,b), where P is new, and a,b are
23
constants. Furthermore make P a minimal predicate using
24
a set_DomPred declaration (see the SPASS man page). This
25
will force that the final step in the proof is the one that
26
eliminates the P literal and the x will be instantiated accordingly.
27
To make this work it may be necessary to turn off certain reduction
28
rules of SPASS. To get it rid of that, a trick is to extend all
29
predicates in C by a further argument with the variable y and all
30
other occurrences of these predicate with fresh variables.
35
Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach
37
Contact : spass@@mpi-inf.mpg.de
added
removed
doc/texinfo/spassfaq.texi
