E Theorem Prover
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Combinations of Theories for Decidable Fragments of First-Order Logic
- Large theory reasoning with SUMO at CASC
- Relaxed weighted path order in theorem proving
- Blocking and other enhancements for bottom-up model generation methods
- Old or heavy? Decaying gracefully with age/weight shapes
- Restricted combinatory unification
- Herbrand constructivization for automated intuitionistic theorem proving
- The 10th IJCAR automated theorem proving system competition -- CASC-J10
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Heaps and Data Structures: A Challenge for Automated Provers
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Exploring properties of normal multimodal logics in simple type theory with \texttt{Leo-II}
- Set of support, demodulation, paramodulation: a historical perspective
- Bayesian ranking for strategy scheduling in automated theorem provers
- Guiding an automated theorem prover with neural rewriting
- Local reductions for the modal cube
- Fast and slow enigmas and parental guidance
- Coming to terms with quantified reasoning
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- AC simplifications and closure redundancies in the superposition calculus
- Logic for Programming, Artificial Intelligence, and Reasoning
- Scalable fine-grained proofs for formula processing
- Superposition with lambdas
- A neurally-guided, parallel theorem prover
- Tools and Algorithms for the Construction and Analysis of Systems
- Machine learning for first-order theorem proving
- An interactive derivation viewer
- A new methodology for developing deduction methods
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- Automated theorem proving in quasigroup and loop theory
- Efficient theory combination via Boolean search
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- Presenting and explaining Mizar
- Automatic construction and verification of isotopy invariants
- Efficient instance retrieval with standard and relational path indexing
- Theoretical Aspects of Computing – ICTAC 2005
- A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes
- Guiding high-performance SAT solvers with unsat-core predictions
- Extensional higher-order paramodulation in Leo-III
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Lemma Mining over HOL Light
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- Harald Ganzinger's legacy: contributions to logics and programming
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- Using the TPTP Language for Writing Derivations and Finite Interpretations
- Superposition with structural induction
- Formalization of the resolution calculus for first-order logic
- Portfolio theorem proving and prover runtime prediction for geometry
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- scientific article; zbMATH DE number 5850137 (Why is no real title available?)
- MaLeS: a framework for automatic tuning of automated theorem provers
- The higher-order prover \textsc{Leo}-II
- Semantically-guided goal-sensitive reasoning: model representation
- Semi-intelligible Isar proofs from machine-generated proofs
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- A resolution-based calculus for preferential logics
- Automated Inference of Finite Unsatisfiability
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Fingerprint indexing for paramodulation and rewriting
- SOLAR: An automated deduction system for consequence finding
- Automated inference of finite unsatisfiability
- Performance of clause selection heuristics for saturation-based theorem proving
- New results on rewrite-based satisfiability procedures
- Proofs and reconstructions
- Random forests for premise selection
- Things to know when implementing KBO
- System for Automated Deduction (SAD): A Tool for Proof Verification
- Mining the Archive of Formal Proofs
- Extending E prover with similarity based clause selection strategies
- SMELS: satisfiability modulo equality with lazy superposition
- SRASS - A Semantic Relevance Axiom Selection System
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Combining and automating classical and non-classical logics in classical higher-order logics
- A principle for incorporating axioms into the first-order translation of modal formulae.
- Automated proof compression by invention of new definitions
- Classification results in quasigroup and loop theory via a combination of automated reasoning tools.
- A combinator-based superposition calculus for higher-order logic
- From informal to formal proofs in Euclidean geometry
- Selecting the selection
- A comprehensive framework for saturation theorem proving
- Making higher-order superposition work
- A rule-based framework for building superposition-based decision procedures
- Superposition with lambdas
- Using tableau to decide description logics with full role negation and identity
- ATP Cross-Verification of the Mizar MPTP Challenge Problems
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- Computing finite models by reduction to function-free clause logic
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Learning theorem proving components
- The role of entropy in guiding a connection prover
- Towards finding longer proofs
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- Machine learning guidance for connection tableaux
- TacticToe: learning to prove with tactics
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Lightweight relevance filtering for machine-generated resolution problems
This page was built for software: E Theorem Prover
