Kovásznai Gergely: HyperS tableaux - heuristic hyper tableaux. In: Acta cybernetica, (17) 2. pp. 325-338. (2005)
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: | 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 |
