E Theorem Prover
From MaRDI portal
Software:22154
swMATH10187MaRDI QIDQ22154FDOQ22154
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- 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
- MaLeCoP Machine Learning Connection Prover
- nanoCoP: A Non-clausal Connection Prover
- The TPTP World – Infrastructure for Automated Reasoning
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
- The 481 Ways to Split a Clause and Deal with Propositional Variables
- Automatic Proof and Disproof in Isabelle/HOL
- Lemma Mining over HOL Light
- Title not available (Why is that?)
- 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
- Evaluation of Automated Theorem Proving on the Mizar Mathematical Library
- Sledgehammer: Judgement Day
- 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
- One Logic to Use Them All
- 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
- Automated verification of refinement laws
- TacticToe: Learning to Reason with HOL4 Tactics
- A rewriting approach to satisfiability procedures.
- MizAR 40 for Mizar 40
- A learning-based fact selector for Isabelle/HOL
- Hierarchical invention of theorem proving strategies
- Model evolution with equality -- revised and implemented
- Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans
- MPTP-motivation, implementation, first experiments
- Automated Proof Compression by Invention of New Definitions
- HOL(y)Hammer: online ATP service for HOL Light
- The Isabelle/Naproche natural language proof assistant
- Learning-assisted theorem proving with millions of lemmas
- MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
- MPTP 0.2: Design, implementation, and initial experiments
- M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
- Extending SMT solvers to higher-order logic
- Extending Sledgehammer with SMT solvers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- On interpolation in automated theorem proving
- Premise selection for mathematics by corpus analysis and kernel methods
- The model evolution calculus as a first-order DPLL method
- Translating higher-order clauses to first-order clauses
- Implementing a fair monodic temporal logic prover
- First-order logic formalisation of impossibility theorems in preference aggregation
- Automated Reasoning Service for HOL Light
- Frontiers of Combining Systems
- MædMax: a maximal ordered completion tool
- Automated and Human Proofs in General Mathematics: An Initial Comparison
- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
- First-Order Logic Formalisation of Arrow’s Theorem
- Multimodal and intuitionistic logics in simple type theory
- Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14--19, 2013. Proceedings
- Hammer for Coq: automation for dependent type theory
- LEO-II and Satallax on the Sledgehammer test bench
- Invariant and Type Inference for Matrices
- ProofWatch: watchlist guidance for large theories in E
- ATPboost: learning premise selection in binary setting with ATP feedback
- Enhancing ENIGMA given clause guidance
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar
- ${\mathcal{T}}$ -Decision by Decomposition
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Combinations of Theories for Decidable Fragments of First-Order Logic
- Title not available (Why is that?)
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Formal Mathematics on Display: A Wiki for Flyspeck
- 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 Deduction – CADE-19
- 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
This page was built for software: E Theorem Prover
