Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!cis.ohio-state.edu!ucbvax!sce.carleton.ca!pearce
From: pearce@sce.carleton.ca (Trevor Pearce)
Newsgroups: comp.lang.icon
Subject: ICON theorem prover?
Message-ID: <9106281610.AA14293@terminus.sce.carleton.ca>
Date: 28 Jun 91 16:10:16 GMT
Sender: daemon@ucbvax.BERKELEY.EDU
Distribution: inet
Organization: The Internet
Lines: 29


Hello,

I am new to the news group and I am a "beginner" with ICON.  My
research involves a string-oriented software specification technique
and I am interested in experimenting with support tools programmed in
ICON. 

More ambitiously, I am interested in the suitability of ICON for
constructing a first-order logic theorem prover.  (As an introduction
to ICON I programmed a "toy" theorem prover that uses the tableau
method to try to find counter-examples of propositional logic
"theorems". The code is not pretty -- typical of a novice -- but it
seems to work on simple examples.)

I would be glad to communicate with anyone who has experience with (or
is interested in) using ICON to construct a theorem prover.

Regards,

Trevor Pearce

Department of Systems and Computer Engineering
Carleton University
Ottawa, Canada
K1S 5B6

email:   pearce@sce.carleton.ca