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 (14)

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

This page was built for publication: Modular proof systems for partial functions with Evans equality