Ermine516 on InstanceConstructionAndDummyProver
Current stage of development (compare)
jvierling on develop
declare constant 'minus' (compare)
jvierling on develop
Replacement for ND Merge pull request #758 from ge… (compare)
jvierling on develop
Remove extraneous asterisk. Merge pull request #757 from ge… (compare)
jvierling on develop
Alternative version of pushEqua… Merge pull request #756 from ge… (compare)
jvierling on develop
Add helper functions, convenien… Better extractor types. syntacticMGU: more functions and 1 more (compare)
object Example extends scala.App {
implicit var ctx = Context()
ctx += hoc"P{?a}: ?a > o"
ctx += Ti
ctx += hoc"c:i"
val t1 = le"P(x:?a)"
val t2 = le"P(c)"
val Some( subst ) = syntacticMGU( t1, t2 )
require( subst( t1 ) == subst( t2 ) )
}
pos2
supposed to represent?
i1
th formula in clause c1
, we want to rewrite t_
to s_
), the second line describes the other clause that we want to rewrite (i2
th formula in clause c2
). pos2
are positions in c2.conclusion(i2)
that can be unified with t_
(the left-hand side of the equation, if leftToRight
is true). https://github.com/gapt/gapt/blob/2c46e4e159b34fd24969bba15c39b6f02ddbb1a7/core/src/main/scala/gapt/provers/escargot/inferences.scala#L460 These positions are then replaced by the right-hand side of the equation, i.e., mgu(s_)
.
./viper.sh --analytic isaplanner/prop_17.smt2
it fails with a gapt.proofs.gaptic.TacticFailureException
and the message goal is not subsumed by provided proof:
. This also affects at least prop_25, 33 and 34 and is the same for the spind mode. Is this is a known thing?
ExtendedProofDatabase
is to associate proofs with formulas (and to keep track of some definitions and axioms). Technically it should be possible to move all this into the Context
(as a facet), but I think that the proof database is somewhat linked to the LLK format and therefore I would not like to integrate it into the context whose responsibility is to keep track of the logical language and the background theories.