A rewriting approach to satisfiability procedures.
type: Item
instance of: scholarly article
title: A rewriting approach to satisfiability procedures.
zbMATH Open document ID: 1054.68077
DOI: 10.1016/S0890-5401(03)00020-8
author: Alessandro Armando
author: Silvio Ranise
author: Michaël Rusinowitch
published in: Information and Computation
publication date: 2003-08-19T00:00:00Z
Mathematics Subject Classification ID: 68Q42
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 1967123
zbMATH Keywords: Automated deduction
zbMATH Keywords: Equational logic
zbMATH Keywords: Term rewriting
zbMATH Keywords: Superposition
zbMATH Keywords: Decision procedures
zbMATH Keywords: Lists
zbMATH Keywords: Encryption
zbMATH Keywords: Arrays with extensionality
zbMATH Keywords: Finite sets with extensionality
zbMATH Keywords: Homomorphism
describes a project that uses: HOL
describes a project that uses: ML
describes a project that uses: Coq
describes a project that uses: PVS
describes a project that uses: E Theorem Prover
MaRDI profile type: Publication
cites work: A practical extension mechanism for decision procedures: The case study of universal Presburger arithmetic
cites work: Q4785507
cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification
cites work: Q4518873
cites work: Q2723409
cites work: Automated complexity analysis based on ordered resolution
cites work: Completion procedures as semidecision procedures
cites work: Towards a foundation of completion procedures as semidecision procedures
cites work: Q3490989
cites work: Q4385532
cites work: Variations on the Common Subexpression Problem
cites work: Q4052071
cites work: Q5287513
cites work: Q3028369
cites work: A complete proof of correctness of the Knuth-Bendix completion algorithm
cites work: Shostak's congruence closure as completion
cites work: Q5581665
cites work: On word problems in Horn theories
cites work: Q4268482
cites work: THE WORD PROBLEM OF ACD-GROUND THEORIES IS UNDECIDABLE
cites work: Any ground associative-commutative theory has a finite canonical system
cites work: Fast Decision Procedures Based on Congruence Closure
cites work: Simplification by Cooperating Decision Procedures
cites work: Paramodulation-based theorem proving
cites work: Proof lengths for equational completion
cites work: Theorem-proving with resolution and superposition
cites work: Q4539621
cites work: Deciding Combinations of Theories
cites work: Q4773298
full work available at URL: s0890-5401(03)00020-8
OpenAlex ID: W2156915267
Recommended article: Frontiers of Combining Systems
Recommended article: New results on rewrite-based satisfiability procedures
Recommended article: Rewrite-based satisfiability procedures for recursive data structures
Recommended article: Automatic Combinability of Rewriting-Based Satisfiability Procedures
Recommended article: Q5446175
Recommended article: A rewrite approach for constraint logic programming
Recommended article: An approach to declarative programming based on a rewriting logic
Recommended article: Rewriting, Inference, and Proof
Recommended article: Q2778866
Recommended article: Rewriting Techniques and Applications
description: scientific article; zbMATH DE number 1967123