The following pages link to E Theorem Prover (Q22154):
Displaying 50 items.
- MaLeS: a framework for automatic tuning of automated theorem provers (Q286787) (← links)
- MizAR 40 for Mizar 40 (Q286800) (← links)
- The higher-order prover \textsc{Leo}-II (Q287283) (← links)
- Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- First-order logic formalisation of impossibility theorems in preference aggregation (Q373021) (← links)
- Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14--19, 2013. Proceedings (Q383830) (← links)
- Model evolution with equality -- revised and implemented (Q429586) (← links)
- Automated inference of finite unsatisfiability (Q438540) (← links)
- Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans (Q475379) (← links)
- Learning-assisted theorem proving with millions of lemmas (Q485842) (← links)
- Consequence-based and fixed-parameter tractable reasoning in description logics (Q490523) (← links)
- MPTP-motivation, implementation, first experiments (Q556682) (← links)
- Combining and automating classical and non-classical logics in classical higher-order logics (Q656826) (← links)
- Fast and slow enigmas and parental guidance (Q831937) (← links)
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments (Q841684) (← links)
- Things to know when implementing KBO (Q861708) (← links)
- M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures (Q862395) (← links)
- MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics (Q865631) (← links)
- \textit{Theorema}: Towards computer-aided mathematical theory exploration (Q865646) (← links)
- MPTP 0.2: Design, implementation, and initial experiments (Q877826) (← links)
- Automatic construction and verification of isotopy invariants (Q928664) (← links)
- Lightweight relevance filtering for machine-generated resolution problems (Q1006731) (← links)
- Computing finite models by reduction to function-free clause logic (Q1006733) (← links)
- Automated verification of refinement laws (Q1037397) (← links)
- A new methodology for developing deduction methods (Q1037405) (← links)
- A rewriting approach to satisfiability procedures. (Q1401930) (← links)
- A formally verified interpreter for a shell-like programming language (Q1630019) (← links)
- Towards a unified ordering for superposition-based automated reasoning (Q1662244) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- Superposition with structural induction (Q1687553) (← links)
- Semantically-guided goal-sensitive reasoning: inference system and completeness (Q1707598) (← links)
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas (Q1735326) (← links)
- On the independence of axioms in BL and MTL (Q1759710) (← links)
- ProofWatch: watchlist guidance for large theories in E (Q1791167) (← links)
- Enhancing ENIGMA given clause guidance (Q1798957) (← links)
- An assumption-based approach for solving the minimal S5-satisfiability problem (Q1799062) (← links)
- Superposition for \(\lambda\)-free higher-order logic (Q1799065) (← links)
- A generic framework for implicate generation modulo theories (Q1799090) (← links)
- Efficient encodings of first-order Horn formulas in equational logic (Q1799100) (← links)
- MædMax: a maximal ordered completion tool (Q1799107) (← links)
- A resolution-based calculus for preferential logics (Q1799110) (← links)
- ATPboost: learning premise selection in binary setting with ATP feedback (Q1799117) (← links)
- LEO-II and Satallax on the Sledgehammer test bench (Q1948289) (← links)
- HOL(y)Hammer: online ATP service for HOL Light (Q2018657) (← links)
- TacticToe: learning to prove with tactics (Q2031416) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Superposition with first-class booleans and inprocessing clausification (Q2055873) (← links)
