Waldmeister
From MaRDI portal
Software:31394
swMATH19568MaRDI QIDQ31394FDOQ31394
Author name not available (Why is that?)
Cited In (47)
- 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
- History and Prospects for First-Order Automated Deduction
- Title not available (Why is that?)
- On using ground joinable equations in equational theorem proving
- Efficient instance retrieval with standard and relational path indexing
- Dependently Typed Programming Based on Automated Theorem Proving
- KI 2004: Advances in Artificial Intelligence
- Computer-assisted human-oriented inductive theorem proving by descente infinie--a manifesto
- 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
- 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
- Relational Lattices via Duality
- Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27--30, 2002. Proceedings
- Varieties of regular semigroups with uniquely defined inversion
- Extended feature algebra
- Perfect Discrimination Graphs: Indexing Terms with Integer Exponents
- Automated Reasoning with Analytic Tableaux and Related Methods
- Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
- Knowledge-based proof planning
- Complete axiomatizations for XPath fragments
- On Transfinite Knuth-Bendix Orders
- Limited resource strategy in resolution theorem proving
- Title not available (Why is that?)
- Proof planning with multiple strategies
- Computer Runtimes and the Length of Proofs
- The CADE-28 Automated Theorem Proving System Competition – CASC-28
- A comprehensive framework for saturation theorem proving
- Efficient encodings of first-order Horn formulas in equational logic
- Ground joinability and connectedness in the superposition calculus
- Detection of First Order Axiomatic Theories
- Knuth-Bendix completion of theories of commuting group endomorphisms
- Unifying Theories of Programming in Isabelle
- Rewrite rules for \(\mathrm{CTL}^\ast\)
- Proof simplification and automated theorem proving
This page was built for software: Waldmeister
