Linearity and regularity with negation normal form
type: Item
instance of: scholarly article
title: Linearity and regularity with negation normal form
zbMATH Open document ID: 1071.68091
author: Reiner Hähnle
author: Neil V. Murray
author: Erik Rosenthal
published in: Theoretical Computer Science
publication date: 2005-01-11T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 2126079
zbMATH Keywords: Automated theorem proving
zbMATH Keywords: Negation normal form
zbMATH Keywords: Resolution
zbMATH Keywords: Linear resolution
zbMATH Keywords: Non-clausal resolution
zbMATH Keywords: Tableaux
zbMATH Keywords: Regular tableaux
zbMATH Keywords: Excess literal technique
MaRDI profile type: Publication
full work available at URL: j.tcs.2004.09.001
OpenAlex ID: W2070794501
cites work: A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
cites work: Theorem Proving via General Matings
cites work: Resolution theorem proving
cites work: Model elimination without contrapositives
cites work: On Matrices with Connections
cites work: Q4935259
cites work: A Computing Procedure for Quantification Theory
cites work: Q4863622
cites work: Tableaux and related methods
cites work: Q4366602
cites work: Linear resolution with selection function
cites work: Q4139711
cites work: A Deductive Approach to Program Synthesis
cites work: Special relations in automated deduction
cites work: Completely non-clausal theorem proving
cites work: Inference with path resolution and semantic graphs
cites work: Dissolution
cites work: A theory of diagnosis from first principles
cites work: Q5591533
cites work: Q5624684
cites work: Q5560258
cites work: Q4860660
DOI: 10.1016/J.TCS.2004.09.001
description: scientific article; zbMATH DE number 2126079