E Theorem Prover

swMATH10187MaRDI QIDQ22154FDOQ22154

Author name not available (Why is that?)

Described by source

• Faster, higher, stronger: E 2.3
• System description: E 1.8
• Automated Reasoning
• Unnamed Publication
• Unnamed Publication

Cited In (only showing first 100 items - show all)

• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• 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}
• Coming to terms with quantified reasoning
• Hammering Mizar by Learning Clause Guidance (Short Paper).
• Scalable fine-grained proofs for formula processing
• Superposition with lambdas
• Fast and slow enigmas and parental guidance
• Tools and Algorithms for the Construction and Analysis of Systems
• An interactive derivation viewer
• Automated theorem proving in quasigroup and loop theory
• A new methodology for developing deduction methods
• ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
• Theoretical Aspects of Computing – ICTAC 2005
• SMELS: Satisfiability Modulo Equality with Lazy Superposition
• Using the TPTP Language for Writing Derivations and Finite Interpretations
• Portfolio theorem proving and prover runtime prediction for geometry
• Superposition with structural induction
• Formalization of the resolution calculus for first-order logic
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Fingerprint indexing for paramodulation and rewriting
• A resolution-based calculus for preferential logics
• Performance of clause selection heuristics for saturation-based theorem proving
• Random forests for premise selection
• Things to know when implementing KBO
• A principle for incorporating axioms into the first-order translation of modal formulae.
• Reliable reconstruction of fine-grained proofs in a proof assistant
• A combinator-based superposition calculus for higher-order logic
• Teaching Automated Theorem Proving by Example: PyRes 1.2
• Computing finite models by reduction to function-free clause logic
• Machine learning guidance for connection tableaux
• TacticToe: learning to prove with tactics
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• The TPTP typed first-order form with arithmetic
• ENIGMA: efficient learning-based inference guiding machine
• Title not available (Why is that?)
• Monte Carlo tableau proof search
• On the independence of axioms in BL and MTL
• Relational characterisations of paths
• Towards a unified ordering for superposition-based automated reasoning
• Theory and Applications of Relational Structures as Knowledge Instruments
• Encoding monomorphic and polymorphic types
• System description: E.T. 0.1
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• A Modal-Layered Resolution Calculus for K
• An assumption-based approach for solving the minimal S5-satisfiability problem
• A generic framework for implicate generation modulo theories
• Superposition for \(\lambda\)-free higher-order logic
• An application of automated reasoning in natural language question answering
• Efficient encodings of first-order Horn formulas in equational logic
• Consequence-based and fixed-parameter tractable reasoning in description logics
• Perfect discrimination graphs: indexing terms with integer exponents
• Automated Reasoning
• Ground joinability and connectedness in the superposition calculus
• First-order resolution methods for modal logics
• Formal mathematics on display: a wiki for Flyspeck
• Automated Reasoning About Metric and Topology
• A formally verified interpreter for a shell-like programming language
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
• Caper
• Hammering towards QED
• Proof simplification and automated theorem proving
• \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
• Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps
• Herbrand constructivization for automated intuitionistic theorem proving
• Machine learning for first-order theorem proving
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Efficient theory combination via Boolean search
• A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes
• Automatic construction and verification of isotopy invariants
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• Lemma Mining over HOL Light
• Title not available (Why is that?)
• Automated Inference of Finite Unsatisfiability
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• 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
• SOLAR: An automated deduction system for consequence finding
• New results on rewrite-based satisfiability procedures
• System for Automated Deduction (SAD): A Tool for Proof Verification
• Mining the Archive of Formal Proofs
• Automated inference of finite unsatisfiability
• SRASS - A Semantic Relevance Axiom Selection System
• Classification results in quasigroup and loop theory via a combination of automated reasoning tools.
• Automated proof compression by invention of new definitions
• Combining and automating classical and non-classical logics in classical higher-order logics
• Using tableau to decide description logics with full role negation and identity
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• Towards finding longer proofs
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Lightweight relevance filtering for machine-generated resolution problems
• Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings
• First-order logic formalisation of Arrow's theorem
• Automated verification of refinement laws
• Invariant and type inference for matrices

This page was built for software: E Theorem Prover