Automated reasoning is fun. E-prover https://github.com/eprover/eprover is a pure C superposition (https://en.wikipedia.org/wiki/Superposition_calculus) theorem prover. It’s quite nice. Superposition (https://www.tcs.ifi.lmu.de/teaching/courses-ws-2024-25/automated-theorem-proving/slides12-superposition.pdf) provers has strengths and weaknesses that complement those of SMT solvers. I was poking around at exporting problems from z3py by printing cnf formulas and reading back in the results using scryerpy, some light bindings I’ve made for scryer prolog (https://github.com/mthom/scryer-prolog), a embeddable rust prolog I’ve made available at pip install kdrag-scryerhttps://github.com/philzook58/scryerpy . This paper pointed out that post processing TPTP stuff via prolog is nice https://arxiv.org/abs/2602.18844 . It is kind of overkill, but it works. Completion via Eprover As time has gone on, I’ve come to understand some of the knobs. It is particularly interesting to me to --print-saturated as this can be used an off the shelf knuth bendix completion (https://en.wikipedia.org/wiki/Knuth%E2%80%93Bendix_completion_algorithm) engine. The equations can be printed in oriented form using the recently added option --print-oriented-eqlits-as-rules. You can also pick the weights --order-weights, precedence of symbols --precedence , and LPO vs KBO term ordering --term-ordering via command line options. Knuth bendix completion can be used as a egraph engine https://www.philipzucker.com/egraph2024_talk/ or egraph modulo theory prototyping engine, so that’s pretty intriguing too. The completion of ground equations is an egraph. Throwing some rules on top of your ground equations with the right ordering can sometimes get you an egraph modulo that theory. eprover has has some special smarts for AC. I don’t know that anyone has thoroughly investigated using this. Here is the classic example of completing the rewrites describing a group With the following command line, we print the completed saturated set as oriented rewrites It is jumping through hoops, but the full loop from z3py expressions into a CNF file, and then parsing back using scyrer prolog and turning back into z3py expressions is in this code https://github.com/philzook58/knuckledragger/blob/101dbcef06fbcc214b90615be752ee070b23b1f0/src/kdrag/solvers/scryer.py . I used the operator precedences file from leancop as prelude, as prolog by default does not parse some tptp operators. Scryer is kind of overkill for this, but if it works it works. I may want to do some light elabrational theorem proving inside scryer to help me reconstruct certificates. One tricky bit is coming from untyped prolog back into typed z3. I can store all the funcdecls, which helps a lot with the type inference problem. I did kind of super lite bidirectional typing in the form of an optional sort=None keyword paramater for what sort is expected. This helps propagate sort information downwards. Generally speaking, this was simple, but a more declarative or constraint producing approach will be able to infer types for more expressions. Note this is outrageuosly faster than my homegrown KB in python https://www.philipzucker.com/knuth_bendix_knuck/ . This problem is baby shit, but even for this my solver took about 1s after I tuned quite a bit. eprover eats it instantaneously. Probably all the time is in making a subprocess etc. Replaying Proof Objects In Knuckederagger, I maintain the right to just trust eprover as an oracle. But it is cool to reconstruct the proof object in order to reduce reliance on trust in my tptp serializers and deserializers. I try to code defensively, but they are definitely buggy. There is probably also some semantics gap between what even in principle what TPTP thinks is true and SMT/z3. I’d also like to work towards converting these proofs (and mine) into exportable metamath 0. Graham’s been firing off on that https://grahamlk.me/Aufbau/#hilbert Here is a problem proving the identity right from the left identity law for a group. It is similar to the above. --proof-object outputs a proof object. The proof object is basically a listing of intermediate provable formulas. The inference rules in the fourth field don’t seem worth trying to take much out of except just the references to the previous theorems. So really the proof object from my perspective is just a DAG of formulas which point back to previous nodes. Reconstructing this take a few moments thought because the goal really has a different status than the by information (being currently unproven). What I need to do is weaken the incoming axioms to goal |= ax or really |= goal -> ax. Then I can have a reflexive proof object for the goal as goal |= goal. As a final step once I have goal |= false, I can turn this into |= not goal It is important to skolemize yourself before handing it off to the prover. I think there is some format for getting information about how the prover skolemized, but skoemization isn’t a theorem, it’s a equisatisfiability / conservative extension thing. |= exists a, foo(a) does not imply by logical reasoning that |= foo(biz). It’s kind of a meta move that you can create a new constant and assert as a new axiom that foo(biz) holds. This is different from |= p /\ q actually can derive |= p without any meta playing or |= forall a, foo(a) can derive |= foo(bar) without any metaplay. ⊨Not(mul(x, inv(x)) != e) If I give the same problem to z3 raw, it does not solve, so we are getting some delta here. The incomplete e-matching is not sufficient for this problem. It needs the clue terms in the eprover proof trace or a more fine grained manual proof. Bits and Bobbles Vampire and eprover are two top tier automated theorem provers. Should I being called eprover “The Equational Theorem Prover E”? I think it’s name is E, but I call it eprover. Isabelle’s sledgehammer is crazy good. I should try to understand it better. A funny thing is basically you need a native automated theorem prover in order to digest proofs from others systems. They’ll only ever really give you breadcrumbs. I may want to use scryer to make some leantap or leancop variants to assist proof reconstruction https://formal.kastel.kit.edu/beckert/leantap/https://jens-otten.de/tutorial_tableaux19/ knuth bendix in prolog https://www.metalevel.at/trs/ . I tried getting saturate running https://resources.mpi-inf.mpg.de/SATURATE/Saturate.html . It’s hopeless. Too fancy, too bit rotted. I also think it’s interesting to explore proof by saturation / inductionless induction in eprover. The mere fact of saturation proves consistency of a statement and therefore it is true in the initial term model or something like that. I dunno how I’d even replay those proofs. I think eprover could be used for unbounded bitvector proofs in the manner. sick https://vprover.github.io/vampireGuide/ vampire’s getting good docs. Getting out vampire proof objects should be quite similar. Vampire seems less straightforward to understand it’s saturated objects. Someone is making rust bindings to vampire https://docs.rs/vampire-sys/latest/vampire_sys/ ? Hellllllo nurse. I’ve been playing with eprover again recently because of my increased understanding of the concepts behind it’s command line knobs and the new --print-eqlists-as-oriented-rules flag. Knuth bendix and e-graphs are intimately related. In this vampire for agda paper https://arxiv.org/abs/2602.18844 , they suggest that one should use a prolog to read out the proof objects. Indeed, the TPTP format is prolog syntax, which is useful for those using prolog and non-useful for everyone else. I made some simple python bindings to scryer-prolog, a rust based prolog. My impression is that scryer is conceptually tighter that swi, but swi is much more feature rich. swi already has python bindings in the form of pyswip https://github.com/yuce/pyswip and janus-swi package. However, it’s not quite self contained enough to install these as python packages. You need to install swi separately to get these to work. As stupid as that sounds, that is important to me. Giants stumbling on pebbles. I also do not like how janus is set up. I really wanted it to be my solution. It clearly to my mind has the python access of prolog as a second class concern. My big gripe is basically how shipping terms back over with variables in them is a no go. You need to ground them first on the prolog side. For my preferences, prolog is the second class citizen. I want prolog for specialized solver-like situations and do not consider it a good general purpose programming language replacement. This is partially due to my relative familiarity, but not entirely. No one has a gun to my head for many of the things I do, so the approach needs to spark joy in me. In a strange way, despite the CNF format seeming so primitive, it is the better one to be using for some purposes. It is “closer to the metal” in some respects and kind of more constructive. The very helpful skolemization and normal form routines make getting a proof object out more confusing. I have found e-prover’s knobs to be less confusing if I am not after refutational theorem proving. a little sad from a datalog perspective, but it ain’t wrong. I haven’t really figured out how to https://docs.rs/vampire-prover/latest/vampire_prover/ whoa $\displaystyle \begin{array}{ll} \text{fix} & x_{125} : \mathsf{Int} \ h_{0} & x_{125} > 17 \ h_{1} & y > 24 \ \hline \vdash & (x_{125} > 7) \wedge (\forall x. x + y \geq y) \end{array}$ $\displaystyle (\text{x} >_s \texttt{0x0007}) \rightarrow (\text{x} >_s \texttt{0x0004})$