Gabriel Ebner
Gabriel Ebner
Conceptually, minimal expansion proofs are the first-order analogue to unsat cores in propositional logic. The current method for expansion proof minimization in GAPT (`minimalExpansionSequent`) uses a very simple approach that...
Development is becoming harder and harder since the number and hence runtime of the tests increases steadily. Our [compile server](http://compile.logic.tuwien.ac.at/job/gapt/lastCompletedBuild/testReport/) has a nice overview of the particularly slow tests. I...
- TPTP = problem and derivation files in TPTP syntax - THF = typed higher-order formula (a formula type in TPTP) - TFF = typed first-order formula (a formula type...
I have just refactored the interpolation algorithm a bit. The partition of the sequent is now represented as a `Sequent[Boolean]`. Anyways, when interpolation hits a cut rule, we need to...
Modern SMT solvers can reason modulo a large number of theories, including the theory of quantifiers. Hence, they can also solve first-order problems (although the proof search is usually incomplete)....
VeriT outputs proofs as s-expressions. The current veriT import tries to parse this output as a _string_. As a consequence, it is difficult to maintain or understand, and the error...
Our proof import from external provers such as Vampire, SPASS, etc., is limited to clausal proofs at the moment: we can only (reliably) parse proofs that start from problems in...
Right now we have no way to reductively eliminate atomic cuts if equational inferences are present. The only way to eliminate them at all at the moment is the following...