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
- nanoCoP: A Non-clausal Connection Prover
- 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
- 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
- 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
- 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
- First-order logic formalisation of Arrow's theorem
- Automated verification of refinement laws
- TacticToe: Learning to Reason with HOL4 Tactics
- Invariant and type inference for matrices
- A rewriting approach to satisfiability procedures.
- MizAR 40 for Mizar 40
- A learning-based fact selector for Isabelle/HOL
- Automated reasoning and presentation support for formalizing mathematics in MizAR
- Sledgehammer: judgement day
- Evaluation of automated theorem proving on the Mizar mathematical library
- Automated and human proofs in general mathematics: an initial comparison
- Overview and evaluation of premise selection techniques for large theory mathematics
- 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
- 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
- The TPTP World -- infrastructure for automated reasoning
- MaLeCoP. Machine learning connection prover
- Automatic proof and disproof in Isabelle/HOL
- 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
- 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
- ${\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
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Formal Mathematics on Display: A Wiki for Flyspeck
- 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
This page was built for software: E Theorem Prover
