Heuristics for resolution-based set-theoretic proofs

Thumbnail Image

Files

1998_SACJ_23_Van der Poll.pdf (4.06 MB)

Authors

Van der Poll, JA
Labuschagne, WA

Issue Date

1999

Type

Article

Language

en

Keywords

Heuristics , Problem frames , Resolution , Set theory , Theorem-proving , Z , ZF

Research Projects

Organizational Units

Journal Issue

Alternative Title

Abstract

A formal specification language like Z permits the specifier to construct proofs which corroborate the aptness of the spec­ification. This process may be facilitated by establishing a partnership between the specifier and a suitable automated reasoner. However, Z specifications are essentially set-theoretic and set-theoretic proofs pose demanding challenges to automated reasoners. Taking the OTTER theorem-prover to be representative of resolution-based automated reasoners. We propose a number of heuristics intended to cut down the search space for proofs involving typical set-theoretic structures.

Description

Citation

Van der Poll JA & Labuschagne WA (1999) Heuristics for resolution-based set-theoretic proofs. South African Computer Journal, Number 23, 1999

Publisher

South African Computer Society (SAICSIT)

License

Journal

Volume

Issue

URI

https://uir.unisa.ac.za/handle/10500/24314

PubMed ID

DOI

ISSN

2313-7835

EISSN

Collections

South African Computer Journal 1999(23)