scientific article; zbMATH DE number 1848313
From MaRDI portal
Publication:4785507
zbMath1005.03012MaRDI QIDQ4785507
Silvio Ranise, Alessandro Armando, Michaël Rusinowitch
Publication date: 1 January 2003
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
equational logichomomorphismsuperpositionterm rewritingautomated deductiondecision procedureslistsarrays with extensionality
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Equational classes, universal algebra in model theory (03C05)
Related Items (10)
A rewriting approach to satisfiability procedures. ⋮ Incorporating decision procedures in implicit induction. ⋮ Decision procedures for term algebras with integer constraints ⋮ Superposition as a decision procedure for timed automata ⋮ A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). ⋮ Superposition for Bounded Domains ⋮ Quantifier Elimination and Provers Integration ⋮ Learning Strategies for Mechanised Building of Decision Procedures ⋮ Model-theoretic methods in combined constraint satisfiability ⋮ Combining Equational Reasoning
This page was built for publication:
