Non-Horn clause logic programming
type: Item
instance of: scholarly article
title: Non-Horn clause logic programming
zbMATH Open document ID: 1017.68507
DOI: 10.1016/S0004-3702(97)00007-6
author: Xumin Nie
published in: Artificial Intelligence
publication date: 2003-08-28T00:00:00Z
Mathematics Subject Classification ID: 68N17
zbMATH DE Number: 1972325
zbMATH Keywords: Automated reasoning
zbMATH Keywords: Logic programming
zbMATH Keywords: Non-Horn clause
describes a project that uses: SETHEO
MaRDI profile type: Publication
cites work: A linear-time algorithm for testing the truth of certain quantified Boolean formulas
cites work: Q3919057
cites work: Q4138187
cites work: Q4040797
cites work: Depth-first iterative-deepening: An optimal admissible tree search
cites work: Q4051550
cites work: SETHEO: A high-performance theorem prover
cites work: Renaming a Set of Clauses as a Horn Set
cites work: Q3339245
cites work: A Simplified Format for the Model Elimination Theorem-Proving Procedure
cites work: Near-Horn prolog and beyond
cites work: Q4366603
cites work: A simplified problem reduction format
cites work: Non-Horn clause logic programming without contrapositives
cites work: A sequent-style model elimination strategy and a positive refinement
cites work: The search efficiency of theorem proving strategies
cites work: A comparison of three PROLOG extensions
cites work: Near-Horn Prolog and the ancestry family of procedures
cites work: A Prolog technology theorem prover: Implementation by an extended Prolog compiler
cites work: A Prolog technology theorem prover: A new exposition and implementation in Prolog
full work available at URL: s0004-3702(97)00007-6
OpenAlex ID: W2001027846
description: scientific article; zbMATH DE number 1972325