HyperS tableaux - heuristic hyper tableaux
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 ove...
Saved in:
| Main Author: | |
|---|---|
| Corporate Author: | |
| Format: | Article |
| Published: |
2005
|
| Series: | Acta cybernetica
17 No. 2 |
| Kulcsszavak: | Számítástechnika, Kibernetika |
| Subjects: | |
| Online Access: | http://acta.bibl.u-szeged.hu/12769 |