Change search
ReferencesLink to record
Permanent link

Direct link
An Intuitionistic Predicate Logic Theorem Prover
Number of Authors: 3
1989 (English)Report (Refereed)
Abstract [en]

A complete theorem prover for intuitionistic predicate logic based on the cut-free calculus is presented. It includes a treatment of "quasi-free" identity based on a delay mechanism and a special form of unification. Several important optimizations of the basic algorithm are introduced. The resulting system is available in source form from SICS; an Appendix gives some idea of its performance.

Place, publisher, year, edition, pages
Kista, Sweden: Swedish Institute of Computer Science , 1989, 1. , 67 p.
Series
SICS Research Report, ISSN 0283-3638 ; R89:01
Keyword [en]
intuitionistic predicate logic, theorem proving
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:ri:diva-21330OAI: oai:DiVA.org:ri-21330DiVA: diva2:1041364
Note
Original report number R89001.Available from: 2016-10-31 Created: 2016-10-31

Open Access in DiVA

fulltext(6109 kB)4 downloads
File information
File name FULLTEXT01.pdfFile size 6109 kBChecksum SHA-512
e6d9a2a0b0ec6348ff9b6de6f16fa442b8998270da1e7ce2993dfddd0e6e673a8d1463e8cfe37c15f7b14a2818ca0904ff84988f0c6f29c881bb6d0e2e141749
Type fulltextMimetype application/pdf

Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 4 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

ReferencesLink to record
Permanent link

Direct link