System description: E 1.8
From MaRDI portal
Recommendations
Cited in
(74)- Relaxed weighted path order in theorem proving
- Blocking and other enhancements for bottom-up model generation methods
- Faster, higher, stronger: E 2.3
- Lash 1.0 (system description)
- Fast and slow enigmas and parental guidance
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Scalable fine-grained proofs for formula processing
- Superposition with lambdas
- scientific article; zbMATH DE number 2043541 (Why is no real title available?)
- Automated Reasoning
- Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- Formalization of the resolution calculus for first-order logic
- On structures of regular standard contradictions in propositional logic
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Semantically-guided goal-sensitive reasoning: model representation
- Semi-intelligible Isar proofs from machine-generated proofs
- The Proof Certifier Checkers
- Targeted configuration of an SMT solver
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- scientific article; zbMATH DE number 2090306 (Why is no real title available?)
- Performance of clause selection heuristics for saturation-based theorem proving
- Extending Maximal Completion (Invited Talk)
- Random forests for premise selection
- The anatomy of Equinox -- an extensible automated reasoning tool for first-order logic and beyond (talk abstract)
- Mining the Archive of Formal Proofs
- Extending E prover with similarity based clause selection strategies
- System Description: E- KRHyper
- Internal guidance for Satallax
- Learning theorem proving components
- The role of entropy in guiding a connection prover
- Towards finding longer proofs
- Machine learning guidance for connection tableaux
- Deepalgebra -- an outline of a program
- Relational characterisations of paths
- E Theorem Prover
- Complexity of translations from resolution to sequent calculus
- Contradiction separation based dynamic multi-clause synergized automated deduction
- Formalization of the Resolution Calculus for First-Order Logic
- GRUNGE: a grand unified ATP challenge
- scientific article; zbMATH DE number 1765689 (Why is no real title available?)
- scientific article; zbMATH DE number 1614710 (Why is no real title available?)
- A learning-based fact selector for Isabelle/HOL
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 1765681 (Why is no real title available?)
- System description: E.T. 0.1
- scientific article; zbMATH DE number 1809863 (Why is no real title available?)
- Lemmatization for stronger reasoning in large theories
- Twee: an equational theorem prover
- Implementing Superposition in iProver (System Description)
- Efficient Low-Level Connection Tableaux
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
- Names are not just sound and smoke: word embeddings for axiom selection
- Solving hard Mizar problems with instantiation and strategy invention
- Graph sequence learning for premise selection
- Invariant neural architecture for learning term synthesis in instantiation proving
- Efficient encodings of first-order Horn formulas in equational logic
- On interpolation in automated theorem proving
- Cooperating proof attempts
- Ground joinability and connectedness in the superposition calculus
- Introducing H, an institution-based formal specification and verification language
- Ordered resolution for coalition logic
- History and prospects for first-order automated deduction
- Quantifier-free equational logic and prime implicate generation
- Hammer for Coq: automation for dependent type theory
- Formula normalizations in verification
- System Description: Spass Version 3.0
- Beagle -- a hierarchic superposition theorem prover
- Caper
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- SPASS \& FLOTTER version 0.42
This page was built for publication: System description: E 1.8
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2870167)
