Ermine516 on InstanceConstructionAndDummyProver
Working PLCOP prover integration (compare)
Ermine516 on InstanceConstructionAndDummyProver
changes for rebase make leancop parser a bit more … changes for rebase and 14 more (compare)
Ermine516 on InstanceConstructionAndDummyProver
added deskolemization (compare)
jvierling on develop
remove some unused code and var… (compare)
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.