scientific article; zbMATH DE number 517065

zbMath0793.68127MaRDI QIDQ4282593

Uwe Waldmann, Leo Bachmair, Harald Ganzinger

Publication date: 17 April 1994

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

completenesssuperpositionredundancydecision procedureparamodulationmonadic class

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25)

Related Items (35)

Speedith: a reasoner for spider diagrams ⋮ More problems in rewriting ⋮ Problems in rewriting III ⋮ Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications ⋮ Some new decidability results on positive and negative set constraints ⋮ Set Constraints, Pattern Match Analysis, and SMT ⋮ Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments ⋮ Model building with ordered resolution: Extracting models from saturated clause sets ⋮ Hyperresolution for guarded formulae ⋮ Superposition as a decision procedure for timed automata ⋮ Superposition decides the first-order logic fragment over ground theories ⋮ Superposition for Fixed Domains ⋮ A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). ⋮ Theorem proving in cancellative abelian monoids (extended abstract) ⋮ 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 OCC1N = ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Unification modulo ACUI plus distributivity axioms ⋮ Deciding inclusion of set constants over infinite non-strict data structures ⋮ Symbolic Model Construction for Saturated Constrained Horn Clauses ⋮ First-order definable counting-only queries ⋮ A comprehensive framework for saturation theorem proving ⋮ A method for building models automatically. Experiments with an extension of OTTER ⋮ Rational spaces and set constraints ⋮ Selecting the Selection ⋮ On the relationship between the complexity of decidability and decomposability of first-order theories ⋮ Set constraints in some equational theories ⋮ Decidability and complexity analysis by basic paramodulation ⋮ Labelled splitting ⋮ A new methodology for developing deduction methods ⋮ SGGS decision procedures ⋮ A comprehensive framework for saturation theorem proving ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. II

This page was built for publication: