1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
<html>
<head><title>What_is_a_Mathematical_Logic_lparen_Q_rparen_.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>What is a Mathematical Logic?</h2>
<p>
<img src=proof.gif><p>
A mathematical logic is a formal system of formulas (<b>axioms</B>) and
<b>rules</B> for deriving other formulas, called <b>theorems</B>.<p>
A <b>proof</B> is a derivation of a theorem. To see a concrete proof
tree, click <a href="A_Trivial_Proof.html">here</a>.<p>
Why should you care? The neat thing about Theorems is that they are
``true.'' More precisely, if all the axioms are valid and the rules
are validity preserving, then anything derived from the axioms via the
rules is valid.<p>
So, if you want to determine if some formula is true, <b>prove it</B>.<p>
<a href="What_is_a_Mechanical_Theorem_Prover_lparen_Q_rparen_.html"><img src=flying.gif></a>
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
