HyperS tableaux - heuristic hyper tableaux

Kovásznai, Gergely: HyperS tableaux - heuristic hyper tableaux. In: Acta cybernetica, (17) 2. pp. 325-338. (2005)

[img]
Preview
Cikk, tanulmány, mű
Kovasznai_2005_ActaCybernetica.pdf

Download (162kB) | Preview

Abstract

Several syntactic methods have been constructed to automate theorem proving in first-order logic. The positive (negative) hyper-resolution and the clause tableaux were combined in a single calculus called hyper tableaux in [1]. In this paper we propose a new calculus called hyperS tableaux which overcomes substantial drawbacks of hyper tableaux. Contrast to hyper tableaux, hyperS tableaux are entirely automated and heuristic. We prove the soundness and the completeness of hyperS tableaux. HyperS tableaux are applied in the theorem prover Sofia, which additionally provides useful tools for clause set generation (based on justificational tableaux) and for tableau simplification (based on redundancy), and advantageous heuristics as well. An additional feature is the support of the so-called parametrized theorems, which makes the prover able to give compound answers.

Item Type: Article
Journal or Publication Title: Acta cybernetica
Date: 2005
Volume: 17
Number: 2
ISSN: 0324-721X
Page Range: pp. 325-338
Language: angol
Event Title: Conference for PhD Students in Computer Science, 4., 2004, Szeged
Uncontrolled Keywords: Természettudomány, Informatika
Additional Information: Bibliogr.: p. 337-338.; Abstract
Date Deposited: 2016. Oct. 15. 12:25
Last Modified: 2018. Jun. 05. 14:56
URI: http://acta.bibl.u-szeged.hu/id/eprint/12769

Actions (login required)

View Item View Item