HyperS tableaux - heuristic hyper tableaux

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

Előnézet

Cikk, tanulmány, mű Kovasznai_2005_ActaCybernetica.pdf Letöltés (162kB) | Előnézet

Absztrakt (kivonat)

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.

Mű típusa:	Cikk, tanulmány, mű
Befoglaló folyóirat/kiadvány címe:	Acta cybernetica
Dátum:	2005
Kötet:	17
Szám:	2
ISSN:	0324-721X
Oldalak:	pp. 325-338
Nyelv:	angol
Kiadás helye:	Szeged
Konferencia neve:	Conference for PhD Students in Computer Science (4.) (2004) (Szeged)
Befoglaló mű URL:	http://acta.bibl.u-szeged.hu/38520/
Kulcsszavak:	Számítástechnika, Kibernetika
Megjegyzések:	Bibliogr.: p. 337-338. ; összefoglalás angol nyelven
Szakterület:	01. Természettudományok 01. Természettudományok > 01.02. Számítás- és információtudomány
Feltöltés dátuma:	2016. okt. 15. 12:25
Utolsó módosítás:	2022. jún. 15. 12:25
URI:	http://acta.bibl.u-szeged.hu/id/eprint/12769

Bővebben:

Tétel nézet