The following pages link to System Description: E 1.8 (Q2870167):
Displayed 50 items.
- E Theorem Prover (Q22154) (← links)
- Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
- Fast and slow enigmas and parental guidance (Q831937) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- Semantically-guided goal-sensitive reasoning: inference system and completeness (Q1707598) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Ground joinability and connectedness in the superposition calculus (Q2104507) (← links)
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving (Q2128804) (← links)
- Towards finding longer proofs (Q2142073) (← links)
- The role of entropy in guiding a connection prover (Q2142077) (← links)
- Learning theorem proving components (Q2142080) (← links)
- Introducing \(H\), an institution-based formal specification and verification language (Q2183716) (← 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)
- Blocking and other enhancements for bottom-up model generation methods (Q2303239) (← links)
- GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
- Names are not just sound and smoke: word embeddings for axiom selection (Q2305419) (← links)
- Faster, higher, stronger: E 2.3 (Q2305435) (← links)
- On interpolation in automated theorem proving (Q2352502) (← links)
- Deepalgebra -- an outline of a program (Q2364671) (← links)
- Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving (Q2817933) (← links)
- Internal Guidance for Satallax (Q2817934) (← links)
- Predicate Elimination for Preprocessing in First-Order Theorem Proving (Q2818027) (← links)
- Formalization of the Resolution Calculus for First-Order Logic (Q2829269) (← links)
- Random Forests for Premise Selection (Q2964471) (← links)
- Lemmatization for Stronger Reasoning in Large Theories (Q2964472) (← links)
- Caper (Q2988651) (← links)
- Mining the Archive of Formal Proofs (Q3453102) (← links)
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP (Q3453107) (← links)
- History and Prospects for First-Order Automated Deduction (Q3454079) (← links)
- Quantifier-Free Equational Logic and Prime Implicate Generation (Q3454103) (← links)
- Cooperating Proof Attempts (Q3454105) (← links)
- System Description: E.T. 0.1 (Q3454109) (← links)
- Efficient Low-Level Connection Tableaux (Q3455764) (← links)
- Ordered Resolution for Coalition Logic (Q3455769) (← links)
- The Proof Certifier Checkers (Q3455771) (← links)
- (Q4989394) (← links)
- Implementing Superposition in iProver (System Description) (Q5049017) (← links)
- Extending Maximal Completion (Invited Talk) (Q5089002) (← links)
- Complexity of translations from resolution to sequent calculus (Q5236549) (← links)
- Hammering Mizar by Learning Clause Guidance (Short Paper). (Q5875448) (← links)
- Scalable fine-grained proofs for formula processing (Q5919479) (← links)
- Superposition with lambdas (Q5919500) (← links)
- A multi-clause dynamic deduction algorithm based on standard contradiction separation rule (Q6086313) (← links)
- Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments (Q6149592) (← links)
