Model completeness, covers and superposition

DOI10.1007/978-3-030-29436-6_9MaRDI QIDQ2305411zbMATH OpenOpenAlexFDO

Authors Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin

Publication date 10 March 2020

Full work available at URL https://doi.org/10.1007/978-3-030-29436-6_9

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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

Describes a project that uses

Uses Software

• Cubicle
• Mcmt

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)