coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Craig Ugoretz <craigugoretz AT yahoo.com>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Coq + OCAML = Symbolic abstract math software?
- Date: Thu, 18 Aug 2005 01:08:12 -0700 (PDT)
- Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=Message-ID:Received:Date:From:Subject:To:MIME-Version:Content-Type:Content-Transfer-Encoding; b=NEURHBmMVXjXvvUhAsde9AsCcTfF2ViDWE/0AgTVqDUaqDWrzKZGQja8w1hvYXhexQWwjuUboFWcBmOzUcuDY/qVsTGVFGnDovejskrh1ck+C3rfuQ8OKDcsOUZKvf9zlklw3ZarHH1xIatNGeMprtBgkqLNnHr6chPzWFSrsgU= ;
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello,
Below is a message that I have posted to
mathforge.net and sci.math.symbolic. After doing this,
I thought, "Why aren't I contacting the Coq club?".
Please give it a read through...
Thanks,
Craig
craigugoretz AT yahoo.com
=====================================================
Hello,
My name is Craig Ugoretz, and I have an idea for an
interesting project that I care to share with you. For
the past five months, I have been collaborating with
Dr. Florentin Smarandache and the AKIRA group to
produce a "neutrosophic cognitive map" module for the
AKIRA multi-paradigm AI system. Neutrosophic logic is
a new form of logic that involves the "neutrosophic
components" of probability of truth, probability of
falsehood, and probability of indeterminency to
describe the characteristics of a given statement. It
is a generalization of fuzzy logic, which is a
generalization of classical logic. Websites relating
to neturosophic logic and AKIRA can be found on the
internet.
I have developed a hypothesis regarding the approach
that should be taken to develop the NCM module.
Neutrosophic logic, if fully implemented, relies on
mathematical subject matter in the area of analysis
such as nonstandard analysis and set valued analysis.
These abstract subjects, in my mind, tax the ability
of conventional computer algebra systems to handle.
For this reason, I have been looking at theorem
provers with "program extraction" to do the job. In
particular, I am interested in the Coq theorem prover,
which extracts programs into the OCAML language. These
programs should be able to handle abstract math like a
computer algebra systems handles the type of
mathematics that is commonly used by scientists,
engineers, and mathematicians.
I am looking for mathematically inclined people to
help me with the task of understanding mathematical
material and programming that material into Coq. Since
I anticipate a significant overlap with computer
programming (I am a programmer), I am looking for
programmers as well to create a unqiue sythesis of
talents. I am sincerely looking forward to your
feedback and offers of assistance. Granted, my
compelling hypothesis has yet to be proven, but with
your support, anything can be possible. If you can
refer me to other sources of competencies, I would
appreciate that as well.
Sincerely,
Craig
craigugoretz AT yahoo.com
- [Coq-Club] Coq + OCAML = Symbolic abstract math software?, Craig Ugoretz
Archive powered by MhonArc 2.6.16.