Modular proof systems for partial functions with Evans equality

DOI10.1016/j.ic.2005.10.002zbMath1103.68112OpenAlexW2156103760MaRDI QIDQ2432764

Uwe Waldmann, Harald Ganzinger, Viorica Sofronie-Stokkermans

Publication date: 25 October 2006

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2005.10.002

zbMATH Keywords

modular superposition calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Interpolation systems for ground proofs in automated deduction: a survey, Reasoning without believing: on the mechanisation of presuppositions and partiality, On First-Order Model-Based Reasoning, An Extension of the Knuth-Bendix Ordering with LPO-Like Properties, Superposition decides the first-order logic fragment over ground theories, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, On Combinations of Local Theory Extensions, Hierarchical Reasoning for the Verification of Parametric Systems, Locality Results for Certain Extensions of Theories with Bridging Functions, On Local Reasoning in Verification, On invariant synthesis for parametric systems, Theory decision by decomposition, Applications of Hierarchical Reasoning in the Verification of Complex Systems, Automatic Verification of Combined Specifications: An Overview

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-theoretic methods in combined constraint satisfiability
• Syntacticness, cycle-syntacticness and shallow theories
• Refutational theorem proving for hierarchic first-order theories
• A rewriting approach to satisfiability procedures.
• Cooperation of background reasoners in theory reasoning by residue sharing
• Ordered chaining calculi for first-order theories of transitive relations
• Simplification by Cooperating Decision Procedures
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Polynomial Time Uniform Word Problems
• Combining Non-Stably Infinite Theories
• A mechanization of strong Kleene logic for partial functions
• Automatic recognition of tractability in inference relations
• Automated Reasoning
• Automated Deduction – CADE-20
• Frontiers of Combining Systems
• On the Existence of Free Structures over Universal Classes
• Polynomial-time computation via local inference relations
• The Word Problem for Abstract Algebras
• Embeddability and the Word Problem