From Search to Computation: Redundancy Criteria and Simplification at Work
From MaRDI portal
Publication:4916077
DOI10.1007/978-3-642-37651-1_7zbMath1383.68076OpenAlexW1497345544MaRDI QIDQ4916077
Uwe Waldmann, Christoph Weidenbach, Ruzica Piskac, Th. Hillenbrand
Publication date: 19 April 2013
Published in: Programming Logics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-37651-1_7
Related Items
Logical reduction of metarules ⋮ Handling transitive relations in first-order automated reasoning ⋮ Subsumption demodulation in first-order theorem proving ⋮ Set of support, demodulation, paramodulation: a historical perspective
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Theorem-proving with resolution and superposition
- A completion procedure for conditional equations
- Equational completion in order-sorted algebras
- Order-sorted completion: The many-sorted way
- More Church-Rosser proofs (in Isabelle/HOL)
- Superposition with equivalence reasoning and delayed clause normal form transformation
- Automated complexity analysis based on ordered resolution
- First-Order Atom Definitions Extended
- Ordered chaining calculi for first-order theories of transitive relations
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Variations on the Common Subexpression Problem
- Software reliability via run-time result-checking
- Translation Methods for Non-Classical Logics: An Overview
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Term Rewriting and All That
- A Theory of Positive Integers in Formal Logic. Part I
- Automatic recognition of tractability in inference relations
- Parallel reductions in \(\lambda\)-calculus
