The following pages link to E Theorem Prover (Q22154):
Displaying 50 items.
- Reliable reconstruction of fine-grained proofs in a proof assistant (Q2055877) (← links)
- The Isabelle/Naproche natural language proof assistant (Q2055899) (← links)
- A combinator-based superposition calculus for higher-order logic (Q2096452) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- Local is best: efficient reductions to modal logic \textsf{K} (Q2102930) (← links)
- Ground joinability and connectedness in the superposition calculus (Q2104507) (← links)
- Local reductions for the modal cube (Q2104538) (← links)
- Bayesian ranking for strategy scheduling in automated theorem provers (Q2104545) (← links)
- Guiding an automated theorem prover with neural rewriting (Q2104548) (← links)
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving (Q2128804) (← links)
- Towards finding longer proofs (Q2142073) (← links)
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search (Q2142075) (← links)
- AC simplifications and closure redundancies in the superposition calculus (Q2142076) (← links)
- The role of entropy in guiding a connection prover (Q2142077) (← links)
- Learning theorem proving components (Q2142080) (← links)
- A neurally-guided, parallel theorem prover (Q2180215) (← links)
- Herbrand constructivization for automated intuitionistic theorem proving (Q2180528) (← links)
- Guiding high-performance SAT solvers with unsat-core predictions (Q2181943) (← links)
- Introducing \(H\), an institution-based formal specification and verification language (Q2183716) (← links)
- Blending under deconstruction. The roles of logic, ontology, and cognition in computational concept invention (Q2188772) (← links)
- Contradiction separation based dynamic multi-clause synergized automated deduction (Q2198231) (← links)
- Relaxed weighted path order in theorem proving (Q2209265) (← links)
- Relational characterisations of paths (Q2210868) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Automating free logic in HOL, with an experimental application in category theory (Q2303232) (← links)
- Blocking and other enhancements for bottom-up model generation methods (Q2303239) (← links)
- Combining induction and saturation-based theorem proving (Q2303240) (← links)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
- Restricted combinatory unification (Q2305407) (← links)
- GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) (Q2305414) (← links)
- Names are not just sound and smoke: word embeddings for axiom selection (Q2305419) (← links)
- Old or heavy? Decaying gracefully with age/weight shapes (Q2305433) (← links)
- Induction in saturation-based proof search (Q2305434) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- SMELS: satisfiability modulo equality with lazy superposition (Q2351265) (← links)
- Machine learning for first-order theorem proving (Q2351414) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Premise selection for mathematics by corpus analysis and kernel methods (Q2352489) (← links)
- On interpolation in automated theorem proving (Q2352502) (← links)
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry (Q2354917) (← links)
- Deepalgebra -- an outline of a program (Q2364671) (← links)
- ENIGMA: efficient learning-based inference guiding machine (Q2364687) (← links)
- The model evolution calculus as a first-order DPLL method (Q2389629) (← links)
- Detecting inconsistencies in large first-order knowledge bases (Q2405258) (← links)
- Monte Carlo tableau proof search (Q2405274) (← links)
- Efficient theory combination via Boolean search (Q2432765) (← links)
- Translating higher-order clauses to first-order clauses (Q2471742) (← links)
- Efficient instance retrieval with standard and relational path indexing (Q2486586) (← links)
- From informal to formal proofs in Euclidean geometry (Q2631958) (← links)
