Treating true/false as atoms can easily lead to bugs: e.g. gapt/gapt#309 If they are not atoms, it's clear that you need to treat them specially.
You can integrate clausification into the saturation loop using this inference: https://github.com/gapt/gapt/blob/2c46e4e159b34fd24969bba15c39b6f02ddbb1a7/core/src/main/scala/gapt/provers/escargot/inferences.scala#L179
But for first-order problems, clausification happens before the main loop is even started.
@gebner At https://github.com/gapt/gapt/blob/2c46e4e159b34fd24969bba15c39b6f02ddbb1a7/core/src/main/scala/gapt/provers/escargot/inferences.scala#L454 what are the positions
pos2 supposed to represent?
The first line of the function arguments describes the equation (
i1th formula in clause c1, we want to rewrite t_ to s_), the second line describes the other clause that we want to rewrite (i2th 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_).
If I run
./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?
I can interrupt it though if it's urgent.
@quicquid I have rebased your commit 287a164656bc60a806d63e3b12f2bf06cc3749c4 on develop. I also did two commits on your 'push_version_2.13.3' branch (these are now on develop as well) before I noticed that the branch is not a feature branch. You can now remove these commits from your branch. Please delete the 'push_version_2.13.3' branch when you are done with it.
@jvierling hi jannik, thank you very much! just a question: i had to rewrite infix binary operators to explicit form, i.e. update + (x,y) to update.+(x,y) because apparently, scala 3 will get extensionality and won't be able to decide if it should curry the function or not. It's a bit ugly because it still works for infix unary functions but i guess renaming + is also not much more readable.
@quicquid As far as I see there are at least two solutions to this problem: 1) We let the method + (of the class PreSubstitution) accept Pairs or 2) As you have already pointed out we could rename +. The first option has the disadvantage that it becomes more difficult to speak about the "two" parameters of the function i.e. it obfuscates the method signature. The second option has the disadvantage that it makes the code less concise but on the other hand we could choose a name that conveys more semantic information (such as e.g. 'extend' or 'extendBy'). Such method names are quite readable but do not fit in well with the functional style.
To be honest I don't know much about the LLK format. As far as I see, the only purpose of
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.
I introduced LLK when I started my thesis ages ago and it has been superseded by Gaptic since. One of my aims is to get rid of it (which should make maintenance of GAPT easier) and transfer all code needing it to Gaptic. I had some time this summer to rewrite my old proofs and they've become much shorter in terms of inferences ( https://derivation.org/nTape2old.png vs. https://derivation.org/nTape2new.png ) but they also take less effort to describe (800 lines vs 250 lines) :-) I'd still like to preserve the old formalization for comparison and documuntation, but we have the JSON format for that now.
I'm currently adapting the cut-elimination code to the new proofs (the hol2fol encoding that just erases types doesn't work with the new version) and would like to make a pull request once everything works again, if that's ok :)
I forgot the procedure. it has been too long.