SETHEO: A high-performance theorem prover
type: Item
instance of: scholarly article
title: SETHEO: A high-performance theorem prover
zbMATH Open document ID: 0759.68080
DOI: 10.1007/BF00244282
author: S. Singh
published in: Journal of Automated Reasoning
publication date: 1992-09-27T00:00:00Z
review text: The paper deals with a theoretical background and practical knowledge of the implementation of the interesting system SETHEO --- a theorem prover for first order logic. The system is based on the connection method and is proved to be sound and complete. SETHEO can be used as an interpreter for the programming language LOP (under development). The inference machine of the system is implemented using Prolog technology, but there are some special characteristics differing SETHEO from common Prolog systems: a powerful preprocessing module for a reduction of the input formula, the proof procedure is realized as a WAM, factorization, lemma generation and the application of proof schemata are offered as options. The entire system is implemented in the language \(C\) and is running on several machines. The important feature of SETHEO is its performance of up to 70 Klips on a SUN SPARC station 1 with 12 Mips.
reviewed by: Josef Šajda
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 57766
zbMATH Keywords: model elimination
zbMATH Keywords: abstract machine technology
zbMATH Keywords: first order logic
zbMATH Keywords: connection method
zbMATH Keywords: Prolog
zbMATH Keywords: preprocessing
describes a project that uses: SETHEO
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/bf00244282
OpenAlex ID: W2084894656
description: scientific article; zbMATH DE number 57766