Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
From MaRDI portal
Publication:2051565
DOI10.1007/s10817-021-09596-xOpenAlexW3173669304MaRDI QIDQ2051565
Marco Montali, Diego Calvanese, Silvio Ghilardi, Andrey Rivkin, Alessandro Gianola
Publication date: 24 November 2021
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-021-09596-x
coversmodel completenessuniform interpolationsuperposition calculusverification of data-aware processes
Related Items
Combination of uniform interpolants via Beth definability ⋮ MODEL COMPLETIONS FOR UNIVERSAL CLASSES OF ALGEBRAS: NECESSARY AND SUFFICIENT CONDITIONS
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Model-theoretic methods in combined constraint satisfiability
- Fast congruence closure and extensions
- Uniform interpolation and propositional quantifiers in modal logics
- Model theory.
- Model-companions and definability in existentially complete structures
- Refutational theorem proving for hierarchic first-order theories
- An algebraic theory of normal forms
- Model completions and r-Heyting categories
- Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
- Interpolation, amalgamation and combination (the non-disjoint signatures case)
- Uniform interpolation and coherence
- Theorem proving with ordering and equality constrained clauses
- Basic paramodulation
- Undefinability of propositional quantifiers in the modal system S4
- From model completeness to verification of data aware processes
- Model completeness, covers and superposition
- Uniform interpolation and compact congruences
- A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
- Modularity results for interpolation, amalgamation and superamalgamation
- On the metamathematics of algebra
- On Interpolation and Symbol Elimination in Theory Extensions
- Generalized Property Directed Reachability
- Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
- Data Structures with Arithmetic Constraints: A Non-disjoint Combination
- Fast Decision Procedures Based on Congruence Closure
- On an interpretation of second order quantification in first order intuitionistic propositional logic
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Shostak's congruence closure as completion
- Monadic second order logic as the model companion of temporal logic
- Term Rewriting and All That
- A sheaf representation and duality for finitely presented Heyting algebras
- Hierarchic Superposition with Weak Abstraction
- SMT-based verification of data-aware processes: a model-theoretic approach
- Interpolation and Symbol Elimination
- Quantifier-free interpolation in combinations of equality interpolating theories
- Cover Algorithms and Their Combination
- Frontiers of Combining Systems
- A MODEL-THEORETIC CHARACTERIZATION OF MONADIC SECOND ORDER LOGIC ON INFINITE WORDS
- MCMT: A Model Checker Modulo Theories
- Lazy Abstraction with Interpolants
- Perspectives of System Informatics
