scientific article; zbMATH DE number 517065
From MaRDI portal
Publication:4282593
Recommendations
Cited in
(39)- Labelled splitting
- A new methodology for developing deduction methods
- Decidability and complexity analysis by basic paramodulation
- Model building with ordered resolution: Extracting models from saturated clause sets
- Hyperresolution for guarded formulae
- Unification modulo ACUI plus distributivity axioms
- Cancellative Abelian monoids and related structures in refutational theorem proving. II
- Superposition as a decision procedure for timed automata
- Superposition decides the first-order logic fragment over ground theories
- On the relationship between the complexity of decidability and decomposability of first-order theories
- SGGS decision procedures
- SCL(EQ): SCL for first-order logic with equality
- Speedith: a reasoner for spider diagrams
- Selecting the selection
- A rule-based framework for building superposition-based decision procedures
- Second-order quantifier elimination on relational monadic formulas -- a basic method and some less expected applications
- Superposition for Fixed Domains
- Theorem proving in cancellative abelian monoids (extended abstract)
- scientific article; zbMATH DE number 1848313 (Why is no real title available?)
- Harald Ganzinger's legacy: contributions to logics and programming
- First-order resolution methods for modal logics
- A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
- More problems in rewriting
- Problems in rewriting III
- Set constraints in some equational theories
- Some new decidability results on positive and negative set constraints
- Rational spaces and set constraints
- Set constraints, pattern match analysis, and SMT
- A method for building models automatically. Experiments with an extension of OTTER
- Deciding inclusion of set constants over infinite non-strict data structures
- A comprehensive framework for saturation theorem proving
- First-order definable counting-only queries
- A comprehensive framework for saturation theorem proving
- SCL(EQ): SCL for first-order logic with equality
- Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- Automatic bit- and memory-precise verification of eBPF code
- First-order automatic literal model generation
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4282593)
