Cited in
(85)- The CADE-28 Automated Theorem Proving System Competition – CASC-28
- Automated Reasoning with Analytic Tableaux and Related Methods
- Extended feature algebra
- A comprehensive framework for saturation theorem proving
- Dependently Typed Programming Based on Automated Theorem Proving
- History and prospects for first-order automated deduction
- Detection of First Order Axiomatic Theories
- Axiomatizing the skew Boolean propositional calculus
- Unifying theories of programming in Isabelle
- Proof simplification and automated theorem proving
- AC simplifications and closure redundancies in the superposition calculus
- Efficient instance retrieval with standard and relational path indexing
- Complete axiomatizations for XPath fragments
- Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27--30, 2002. Proceedings
- Fast and slow enigmas and parental guidance
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Varieties of regular semigroups with uniquely defined inversion
- Semi-intelligible Isar proofs from machine-generated proofs
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Computer supported mathematics with \(\Omega\)MEGA
- Efficient encodings of first-order Horn formulas in equational logic
- Internal axioms for domain semirings
- scientific article; zbMATH DE number 6027911 (Why is no real title available?)
- On transfinite Knuth-Bendix orders
- FTP'2003: 4th international workshop on first-order theorem proving. Proceedings of the workshop (in connection with RDP'03, federated conference on rewriting, deduction and programming), Valencia, Spain, June 12--14, 2003
- Proof planning with multiple strategies
- Relational lattices via duality
- Computer runtimes and the length of proofs. With an algorithmic probabilistic application to waiting times in automatic theorem proving
- Ground joinability and connectedness in the superposition calculus
- SETHEO
- OTTER
- SPASS
- Prover9
- DCTP
- SATCHMO
- AURA
- Things to know when implementing KBO
- SPIKE
- iProver
- Mella
- mkbTT
- SicoTHEO
- Slothrop
- Wolfram Demonstrations
- EQP
- TRAMP
- CLAM
- DISCOUNT
- Lambda-Clam
- LOUI
- Oyster
- SNARK
- Prodigy
- Bliksem
- KOMET
- Multi
- PROTEIN
- Peers-mcd
- Tribe
- QuodLibet
- MadMax
- Twee
- Omega-MKRP
- Network Security Policy Verification
- Ordered_Resolution_Prover
- XPlain
- ACER
- ProverX
- A comprehensive framework for saturation theorem proving
- Limited resource strategy in resolution theorem proving
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- KI 2004: Advances in Artificial Intelligence
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Guiding an automated theorem prover with neural rewriting
- Rewrite rules for \(\mathrm{CTL}^\ast\)
- Computer-assisted human-oriented inductive theorem proving by \textit{descente infinie} -- a manifesto
- scientific article; zbMATH DE number 2043541 (Why is no real title available?)
- Mechanizing Mathematical Reasoning
- Performance of clause selection heuristics for saturation-based theorem proving
- Algebraic separation logic
- On using ground joinable equations in equational theorem proving
- Knowledge-based proof planning
- Knuth-Bendix completion of theories of commuting group endomorphisms
- Perfect discrimination graphs: indexing terms with integer exponents
This page was built for software: Waldmeister
