Model completeness, covers and superposition
From MaRDI portal
Recommendations
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- Cover Algorithms and Their Combination
- From model completeness to verification of data aware processes
- scientific article; zbMATH DE number 1950258
- Superposition for Fixed Domains
Cites work
- A comprehensive combination framework
- A logical reconstruction of reachability
- A model-theoretic characterization of monadic second order logic on infinite words
- A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- Basic paramodulation
- Combinable Extensions of Abelian Groups
- Combining satisfiability procedures for unions of theories with a shared counting operator
- Cover Algorithms and Their Combination
- From model completeness to verification of data aware processes
- Generalized property directed reachability
- Hierarchic superposition with weak abstraction
- Interpolation and Symbol Elimination
- Interpolation, amalgamation and combination (the non-disjoint signatures case)
- Lazy Abstraction with Interpolants
- MCMT: a model checker modulo theories
- Model completeness, covers and superposition
- Model theory.
- Model-companions and definability in existentially complete structures
- Model-theoretic methods in combined constraint satisfiability
- Modularity results for interpolation, amalgamation and superamalgamation
- Monadic second order logic as the model companion of temporal logic
- On an interpretation of second order quantification in first order intuitionistic propositional logic
- Paramodulation-based theorem proving
- Proving refutational completeness of theorem-proving strategies
- Quantifier-free interpolation in combinations of equality interpolating theories
- Refutational theorem proving for hierarchic first-order theories
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
- Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
- Shostak's congruence closure as completion
- SMT-based verification of data-aware processes: a model-theoretic approach
- Term Rewriting and All That
- Theorem proving with ordering and equality constrained clauses
Cited in
(7)- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- Combination of uniform interpolants via Beth definability
- Combined covers and Beth definability
- Interpolation and amalgamation for arrays with MaxDiff
- Model completeness, covers and superposition
- scientific article; zbMATH DE number 2120363 (Why is no real title available?)
- SMT-based verification of data-aware processes: a model-theoretic approach
This page was built for publication: Model completeness, covers and superposition
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2305411)