Modular proof systems for partial functions with Evans equality
From MaRDI portal
Publication:2432764
DOI10.1016/J.IC.2005.10.002zbMATH Open1103.68112OpenAlexW2156103760MaRDI QIDQ2432764FDOQ2432764
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
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
- Publication:3490986
- Modal Theorem Proving: An Equational Viewpoint
Cites Work
- Title not available (Why is that?)
- Simplification by Cooperating Decision Procedures
- A rewriting approach to satisfiability procedures.
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Title not available (Why is that?)
- Automatic recognition of tractability in inference relations
- Title not available (Why is that?)
- Ordered chaining calculi for first-order theories of transitive relations
- Polynomial Time Uniform Word Problems
- The Word Problem for Abstract Algebras
- Embeddability and the Word Problem
- Refutational theorem proving for hierarchic first-order theories
- Automated Reasoning
- Model-theoretic methods in combined constraint satisfiability
- Title not available (Why is that?)
- Automated Deduction – CADE-20
- Frontiers of Combining Systems
- Cooperation of background reasoners in theory reasoning by residue sharing
- Combining non-stably infinite theories
- Polynomial-time computation via local inference relations
- Syntacticness, cycle-syntacticness and shallow theories
- A mechanization of strong Kleene logic for partial functions
- On the Existence of Free Structures over Universal Classes
- Title not available (Why is that?)
Cited In (18)
- Locality Results for Certain Extensions of Theories with Bridging Functions
- Modular termination and combinability for superposition modulo counter arithmetic
- Harald Ganzinger's legacy: contributions to logics and programming
- Superposition and Model Evolution Combined
- Interpolation systems for ground proofs in automated deduction: a survey
- On Local Reasoning in Verification
- Superposition modulo a Shostak theory.
- On invariant synthesis for parametric systems
- Theory decision by decomposition
- Applications of hierarchical reasoning in the verification of complex systems
- On First-Order Model-Based Reasoning
- On combinations of local theory extensions
- Hierarchical reasoning for the verification of parametric systems
- Superposition decides the first-order logic fragment over ground theories
- Automated Reasoning
- Reasoning without believing: on the mechanisation of presuppositions and partiality
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- Automatic verification of combined specifications: an overview
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)
