Waldmeister
From MaRDI portal
Software:31394
No author found.
Related Items (47)
Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27--30, 2002. Proceedings ⋮ Computer Runtimes and the Length of Proofs ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ Fast and slow enigmas and parental guidance ⋮ Extended feature algebra ⋮ AC simplifications and closure redundancies in the superposition calculus ⋮ History and Prospects for First-Order Automated Deduction ⋮ Knuth-Bendix completion of theories of commuting group endomorphisms ⋮ Dependently Typed Programming Based on Automated Theorem Proving ⋮ Proof planning with multiple strategies ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ Things to know when implementing KBO ⋮ \textit{Theorema}: Towards computer-aided mathematical theory exploration ⋮ Computer supported mathematics with \(\Omega\)MEGA ⋮ The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 ⋮ 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 ⋮ Axiomatizing the skew Boolean propositional calculus ⋮ Varieties of regular semigroups with uniquely defined inversion ⋮ Unnamed Item ⋮ Unifying Theories of Programming in Isabelle ⋮ Internal axioms for domain semirings ⋮ Limited resource strategy in resolution theorem proving ⋮ On using ground joinable equations in equational theorem proving ⋮ Knowledge-based proof planning ⋮ Mechanizing Mathematical Reasoning ⋮ Rewrite rules for \(\mathrm{CTL}^\ast\) ⋮ Simple and Efficient Clause Subsumption with Feature Vector Indexing ⋮ Computer-assisted human-oriented inductive theorem proving by descente infinie--a manifesto ⋮ Relational Lattices via Duality ⋮ Efficient instance retrieval with standard and relational path indexing ⋮ Algebraic separation logic ⋮ Complete axiomatizations for XPath fragments ⋮ Perfect Discrimination Graphs: Indexing Terms with Integer Exponents ⋮ On Transfinite Knuth-Bendix Orders ⋮ KI 2004: Advances in Artificial Intelligence ⋮ Proof simplification and automated theorem proving ⋮ Efficient encodings of first-order Horn formulas in equational logic ⋮ A comprehensive framework for saturation theorem proving ⋮ Automated Reasoning with Analytic Tableaux and Related Methods ⋮ Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving ⋮ Unnamed Item ⋮ Detection of First Order Axiomatic Theories ⋮ A comprehensive framework for saturation theorem proving ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ Ground joinability and connectedness in the superposition calculus ⋮ Guiding an automated theorem prover with neural rewriting
This page was built for software: Waldmeister
