Theorem-proving with resolution and superposition
type: Item
instance of: scholarly article
title: Theorem-proving with resolution and superposition
zbMATH Open document ID: 0723.68094
DOI: 10.1016/S0747-7171(08)80131-9
published in: Journal of Symbolic Computation
publication date: 1991-01-01T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 4193157
zbMATH Keywords: resolution
zbMATH Keywords: superposition
zbMATH Keywords: complete simplification ordering
zbMATH Keywords: refutational completeness
zbMATH Keywords: paramodulation
author: Michaël Rusinowitch
MaRDI profile type: Publication
cites work: Q5679729
cites work: Orderings for term-rewriting systems
cites work: Termination of rewriting
cites work: A superposition oriented theorem prover
cites work: Unit Refutations and Horn Sets
cites work: Q3786024
cites work: Proving refutational completeness of theorem-proving strategies
cites work: Q3028369
cites work: A complete proof of correctness of the Knuth-Bendix completion algorithm
cites work: On word problems in Horn theories
cites work: Q5581665
cites work: Q3702510
cites work: Q4139711
cites work: Problem corner: Reasoning about equality
cites work: Q3698310
cites work: A Technique for Establishing Completeness Results in Theorem Proving with Equality
cites work: Q5678447
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q5624683
cites work: The Concept of Demodulation in Theorem Proving
description: scientific article; zbMATH DE number 4193157