E Theorem Prover
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Lightweight relevance filtering for machine-generated resolution problems
- Computing finite models by reduction to function-free clause logic
- Automated verification of refinement laws
- A new methodology for developing deduction methods
- Aligator
- ILTP
- LEO-II
- PyRes
- Nitpick
- lazyCoP
- QOCA
- Shellcheck
- CoLiS
- MedleySolver
- Nunchaku
- SOLAR
- TPS
- Hilberticus
- A rewriting approach to satisfiability procedures.
- Isabelle/HOL
- RuleML
- MizarMode
- ToolBus
- AFRA
- MPTP
- MPTP 0.2
- OTTER
- VAMPIRE
- THF0
- Paradox
- SMT-LIB
- SPASS
- A formally verified interpreter for a shell-like programming language
- TPTP
- Darwin
- Metis
- Towards a unified ordering for superposition-based automated reasoning
- Hammer for Coq: automation for dependent type theory
- Formalization of the resolution calculus for first-order logic
- Isar
- SPASS+T
- STRIP
- MoMM
- Mizar
- Superposition with structural induction
- cvc3
- z3
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Prover9
- SIMPLIFY
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
- On the independence of axioms in BL and MTL
- HOL
- ProofWatch: watchlist guidance for large theories in E
- Enhancing ENIGMA given clause guidance
- An assumption-based approach for solving the minimal S5-satisfiability problem
- Superposition for -free higher-order logic
- A generic framework for implicate generation modulo theories
- Efficient encodings of first-order Horn formulas in equational logic
- MædMax: a maximal ordered completion tool
- A resolution-based calculus for preferential logics
- ATPboost: learning premise selection in binary setting with ATP feedback
- ETPS
- FINDER
- TSPASS
- HOL Light
- SATCHMO
- DCTP
- I-SATCHMO
- SCOTT
- Zenon
- Satallax
- E-Darvin
- Mace4
- MML
- Sledgehammer
- ML4PG
- Isabelle/PIDE
- MaLeCoP
- ESC4
- LEO-II and Satallax on the Sledgehammer test bench
- CVC Lite
- LoTREC
- HipSpec
- HOL(y)Hammer: online ATP service for HOL Light
- MaSh
- TacticToe: learning to prove with tactics
- Machine learning guidance for connection tableaux
- Superposition with first-class booleans and inprocessing clausification
- Reliable reconstruction of fine-grained proofs in a proof assistant
- The Isabelle/Naproche natural language proof assistant
- StarExec
- A combinator-based superposition calculus for higher-order logic
- Set of support, demodulation, paramodulation: a historical perspective
- Local is best: efficient reductions to modal logic \textsf{K}
- Ground joinability and connectedness in the superposition calculus
- Local reductions for the modal cube
- Bayesian ranking for strategy scheduling in automated theorem provers
- Guiding an automated theorem prover with neural rewriting
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
This page was built for software: E Theorem Prover
