Modular proof systems for partial functions with Evans equality

DOI10.1016/J.IC.2005.10.002MaRDI QIDQ2432764zbMATH OpenOpenAlexFDO

Authors Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann

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)

Recommendations

• Automated Reasoning
• On the completeness of modular proof systems
• Equational theorem proving modulo
• Theorem Proving Modulo Based on Boolean Equational Procedures
• A Proof of Modular Invariance
• A Proof of a Theorem on Modular Functions
• Extending a Resolution Prover for Inequalities on Elementary Functions
• scientific article; zbMATH DE number 4164168
• Modal Theorem Proving: An Equational Viewpoint

Cites work

• A mechanization of strong Kleene logic for partial functions
• A rewriting approach to satisfiability procedures.
• Automated Deduction – CADE-20
• Automated Reasoning
• Automatic recognition of tractability in inference relations
• Combining non-stably infinite theories
• Cooperation of background reasoners in theory reasoning by residue sharing
• Embeddability and the Word Problem
• Frontiers of Combining Systems
• scientific article; zbMATH DE number 3963900 (Why is no real title available?)
• scientific article; zbMATH DE number 1189060 (Why is no real title available?)
• scientific article; zbMATH DE number 1140674 (Why is no real title available?)
• scientific article; zbMATH DE number 2090311 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• Model-theoretic methods in combined constraint satisfiability
• On the Existence of Free Structures over Universal Classes
• Ordered chaining calculi for first-order theories of transitive relations
• Polynomial Time Uniform Word Problems
• Polynomial-time computation via local inference relations
• Refutational theorem proving for hierarchic first-order theories
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Simplification by Cooperating Decision Procedures
• Syntacticness, cycle-syntacticness and shallow theories
• The Word Problem for Abstract Algebras

Cited in

(18)

• Theory decision by decomposition
• Superposition decides the first-order logic fragment over ground theories
• On invariant synthesis for parametric systems
• Applications of hierarchical reasoning in the verification of complex systems
• Interpolation systems for ground proofs in automated deduction: a survey
• Automatic verification of combined specifications: an overview
• On First-Order Model-Based Reasoning
• Modular termination and combinability for superposition modulo counter arithmetic
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• Reasoning without believing: on the mechanisation of presuppositions and partiality
• Harald Ganzinger's legacy: contributions to logics and programming
• On combinations of local theory extensions
• Superposition and Model Evolution Combined
• Locality Results for Certain Extensions of Theories with Bridging Functions
• Automated Reasoning
• On Local Reasoning in Verification
• Hierarchical reasoning for the verification of parametric systems
• Superposition modulo a Shostak theory.

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2432764)