Model completeness, covers and superposition
From MaRDI portal
Publication:2305411
DOI10.1007/978-3-030-29436-6_9OpenAlexW2969474843MaRDI QIDQ2305411
Alessandro Gianola, Diego Calvanese, Marco Montali, Silvio Ghilardi, Andrey Rivkin
Publication date: 10 March 2020
Full work available at URL: https://doi.org/10.1007/978-3-030-29436-6_9
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
SMT-based verification of data-aware processes: a model-theoretic approach ⋮ Interpolation and amalgamation for arrays with MaxDiff ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Model completeness, covers and superposition ⋮ Combination of uniform interpolants via Beth definability ⋮ Combined covers and Beth definability
Uses Software
Cites Work
- Unnamed Item
- Model-theoretic methods in combined constraint satisfiability
- Model theory.
- Model-companions and definability in existentially complete structures
- Refutational theorem proving for hierarchic first-order theories
- Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
- Interpolation, amalgamation and combination (the non-disjoint signatures case)
- Theorem proving with ordering and equality constrained clauses
- Basic paramodulation
- From model completeness to verification of data aware processes
- Model completeness, covers and superposition
- A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
- Modularity results for interpolation, amalgamation and superamalgamation
- 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
- 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
- Hierarchic Superposition with Weak Abstraction
- SMT-based verification of data-aware processes: a model-theoretic approach
- Combinable Extensions of Abelian Groups
- Interpolation and Symbol Elimination
- A comprehensive combination framework
- Quantifier-free interpolation in combinations of equality interpolating theories
- Cover Algorithms and Their Combination
- 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
