-
Notifications
You must be signed in to change notification settings - Fork 0
Home
Welcome to the Euclid-Automated-Theorem-Prover-JavaScript-Plugin- wiki!
Euclid is separated into two ( 2 ) tools:
( 1 ) An ESL Natural Language Processor, Formal Logic & Reasoning Engine
SAMPLE 1
I am an engineer.
Paul is an engineer.
Who is an engineer ?
SAMPLE 2
I have 5 dogs.
3 dogs are sick.
How many dogs are not sick ?
SAMPLE 3
An engineer is an individual whom applies the discipline of math and science in his daily work.
what is an engineer ?
SAMPLE 4 ( Perform dictionary lookup )
george washington, apple, car
..and..
( 2 ) A Symbol editor and axiom-supported prover (extensible)
SAMPLE 1
x = a
x + y + z = a
x + y + z + b + c = d
Prove a + b + c = d
SAMPLE 2
x over x = 1
x times 0 = 0
x over 0 = undefined
0 over x = 0
sum from { i = 1 } to { N } x _ { i minus 1 } times x _ i = x raised N
Prove { k times { 1 over b } = 1 }
%--------------------------------------------------------------------------
a times b = c
h times b = j
j times { 1 over h } = k
f of x = { 1 } over { sigma sqrt { 2 pi } } e ^ - { { ( x - mu ) ^ 2 } over { 2 sigma ^ 2 } }
newline
newline
C = pi cdot d = 2 cdot pi cdot r
newline
newline
f of x = sum from { i = 0 } to { infinity } { { f raised { ( i ) } ( 0 ) } over { i ! } x raised i }
newline
newline
left [ matrix { 1 # 2 ## 3 # 4 } right ]
..these two (2) tools are the minimum requirements for documenting a state-of-the-art original proof.
In the future Euclid will..
- retrieve dictionary definitions by word-entry or use wildcards (RegularExpressions)
If not Capitalization or punctuation Euclid assumes you're looking for a definition
Euclid also accepts regular-expression and can match multiple words and retrieve their
definitions ([Gg]eorge\s*[Ww]ashington)
- Euclid works offline
- homework problems
- solve riddles
- math proofs (Fermat's Last Theorem)
- formal reasoning
- (automated) theorem proving
- courtroom prep (Best way to present case before a judge)
- parse legal documents
- summarize articles (Q&A)
- Patent Examination (Summary & Verification)
- Food recipe creation (Analyze and meet req's for taste,color,texture)
- Verify output of Regular-Expressions
- Demonstrate $1M Clay Math prize proofs using automated theorem-proving
- Downloadable full version
SYSTEM REQ
51 GB AVAILABLE SPACE
16 GB RAM
HOW EUCLID WORKS (HOW EUCLID BUILDS INTERNAL ASSOCIATIONS..
Euclid maps axioms onto a network topology
Example
Prove { x times b = c }
x = a
a times b = c
INTERNAL REPRESENTATION
a
| (00)
x
a times b (01)
\
/
c
.
.
x
|
a
\
times b (00+01)
\
/
c
Euclid uses axioms that you provide to build an internal representation, or network,
(a connected DiGraph) and iff Euclid can then traverse from x to c,
the theorem is proved.
Notice however that the node is not collapsed any further!
This is to prevent non-determinism (NFA loops)
Operators are never used to associate nodes.
Best strategy for theorem-proving:
Break theorems into proofing steps
Migrate proofing steps into modules
After using Euclid Logic to verify modules which
guarantee semantic coverage, then
Euclid Formula can be used to rigorously, mathematically solve the modules
Updates will be posted here.