swMATH19568MaRDI QIDQ31394FDOQ31394
Author name not available (Why is that?)
Official website: http://www.waldmeister.org/
Cited In (83)
- Dependently Typed Programming Based on Automated Theorem Proving
- Extended feature algebra
- Automated Reasoning with Analytic Tableaux and Related Methods
- The CADE-28 Automated Theorem Proving System Competition – CASC-28
- A comprehensive framework for saturation theorem proving
- Detection of First Order Axiomatic Theories
- Axiomatizing the skew Boolean propositional calculus
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Guiding an automated theorem prover with neural rewriting
- AC simplifications and closure redundancies in the superposition calculus
- Fast and slow enigmas and parental guidance
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Title not available (Why is that?)
- On using ground joinable equations in equational theorem proving
- Efficient instance retrieval with standard and relational path indexing
- KI 2004: Advances in Artificial Intelligence
- Mechanizing Mathematical Reasoning
- Semi-intelligible Isar proofs from machine-generated proofs
- 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
- Performance of clause selection heuristics for saturation-based theorem proving
- Things to know when implementing KBO
- A comprehensive framework for saturation theorem proving
- Algebraic separation logic
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Computer supported mathematics with \(\Omega\)MEGA
- Internal axioms for domain semirings
- Computer runtimes and the length of proofs. With an algorithmic probabilistic application to waiting times in automatic theorem proving
- Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27--30, 2002. Proceedings
- Varieties of regular semigroups with uniquely defined inversion
- SPASS
- Prover9
- DCTP
- SATCHMO
- AURA
- Knowledge-based proof planning
- SPIKE
- iProver
- Mella
- mkbTT
- SicoTHEO
- Slothrop
- Wolfram Demonstrations
- EQP
- Complete axiomatizations for XPath fragments
- 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
- Limited resource strategy in resolution theorem proving
- Computer-assisted human-oriented inductive theorem proving by \textit{descente infinie} -- a manifesto
- Ordered_Resolution_Prover
- XPlain
- ACER
- ProverX
- Unifying theories of programming in Isabelle
- Title not available (Why is that?)
- Relational lattices via duality
- Proof planning with multiple strategies
- Efficient encodings of first-order Horn formulas in equational logic
- Perfect discrimination graphs: indexing terms with integer exponents
- Ground joinability and connectedness in the superposition calculus
- History and prospects for first-order automated deduction
- Knuth-Bendix completion of theories of commuting group endomorphisms
- Rewrite rules for \(\mathrm{CTL}^\ast\)
- Proof simplification and automated theorem proving
- On transfinite Knuth-Bendix orders
This page was built for software: Waldmeister
