HyperS tableaux - heuristic hyper tableaux

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

[thumbnail of Kovasznai_2005_ActaCybernetica.pdf]
Cikk, tanulmány, mű

Download (162kB) | Preview


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: English
Place of Publication: Szeged
Event Title: Conference for PhD Students in Computer Science (4.) (2004) (Szeged)
Related URLs: http://acta.bibl.u-szeged.hu/38520/
Uncontrolled Keywords: Számítástechnika, Kibernetika
Additional Information: Bibliogr.: p. 337-338. ; összefoglalás angol nyelven
Subjects: 01. Natural sciences
01. Natural sciences > 01.02. Computer and information sciences
Date Deposited: 2016. Oct. 15. 12:25
Last Modified: 2022. Jun. 15. 12:25
URI: http://acta.bibl.u-szeged.hu/id/eprint/12769

Actions (login required)

View Item View Item