HyperS tableaux - heuristic hyper tableaux

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

[img] Cikk, tanulmány, mű

Download (162kB)


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
Event Title: Conference for PhD Students in Computer Science, 4., 2004, Szeged
Journal or Publication Title: Acta cybernetica
Date: 2005
Volume: 17
Number: 2
Page Range: pp. 325-338
ISSN: 0324-721X
Language: angol
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