From Search to Computation: Redundancy Criteria and Simplification at Work

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items (4)

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

• Unnamed Item
• SPASS
• E Theorem Prover
• Saturate
• FLOTTER

Cites Work

• 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
• 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

This page was built for publication: From Search to Computation: Redundancy Criteria and Simplification at Work