The following pages link to (Q3150301):
Displaying 50 items.
- E Theorem Prover (Q22154) (← links)
- 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)
- 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)
- MPTP-motivation, implementation, first experiments (Q556682) (← links)
- Combining and automating classical and non-classical logics in classical higher-order logics (Q656826) (← links)
- Things to know when implementing KBO (Q861708) (← 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)
- Automated verification of refinement laws (Q1037397) (← links)
- A new methodology for developing deduction methods (Q1037405) (← links)
- HOL(y)Hammer: online ATP service for HOL Light (Q2018657) (← links)
- TacticToe: learning to prove with tactics (Q2031416) (← links)
- Superposition for full higher-order logic (Q2055874) (← links)
- Reliable reconstruction of fine-grained proofs in a proof assistant (Q2055877) (← links)
- The Isabelle/Naproche natural language proof assistant (Q2055899) (← links)
- A combinator-based superposition calculus for higher-order logic (Q2096452) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- Bayesian ranking for strategy scheduling in automated theorem provers (Q2104545) (← links)
- Guiding an automated theorem prover with neural rewriting (Q2104548) (← links)
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search (Q2142075) (← links)
- AC simplifications and closure redundancies in the superposition calculus (Q2142076) (← links)
- The role of entropy in guiding a connection prover (Q2142077) (← links)
- Learning theorem proving components (Q2142080) (← links)
- \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality (Q2156971) (← links)
- Blending under deconstruction. The roles of logic, ontology, and cognition in computational concept invention (Q2188772) (← links)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) (Q2305414) (← links)
- Old or heavy? Decaying gracefully with age/weight shapes (Q2305433) (← links)
- Induction in saturation-based proof search (Q2305434) (← links)
- Faster, higher, stronger: E 2.3 (Q2305435) (← links)
- SMELS: satisfiability modulo equality with lazy superposition (Q2351265) (← links)
- Machine learning for first-order theorem proving (Q2351414) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Premise selection for mathematics by corpus analysis and kernel methods (Q2352489) (← links)
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry (Q2354917) (← links)
- Deepalgebra -- an outline of a program (Q2364671) (← links)
- Efficient theory combination via Boolean search (Q2432765) (← links)
- Efficient instance retrieval with standard and relational path indexing (Q2486586) (← links)
- From informal to formal proofs in Euclidean geometry (Q2631958) (← links)
- Portfolio theorem proving and prover runtime prediction for geometry (Q2631959) (← links)
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (Q2655326) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- Extracting Higher-Order Goals from the Mizar Mathematical Library (Q2817297) (← links)
