1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
<html>
<head><title>DEFAXIOM.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>DEFAXIOM</h2>add an axiom
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
WARNING: We strongly recommend that you not add axioms. If at all
possible you should use <code><a href="DEFUN.html">defun</a></code> or <code><a href="MUTUAL-RECURSION.html">mutual-recursion</a></code> to define new
concepts recursively or use <code><a href="ENCAPSULATE.html">encapsulate</a></code> to constrain them
constructively. If your goal is to defer a proof by using a
top-down style, consider using <code><a href="SKIP-PROOFS.html">skip-proofs</a></code>; see the discussion
on ``Top-Down Proof'' in Section B.1.2 of ``Computer-Aided
Reasoning: An Approach.'' Adding new axioms frequently renders the
logic inconsistent.
<pre>
Example:
(defaxiom sbar (equal t nil)
:rule-classes nil
:doc ":Doc-Section ...")
<p>
General Form:
(defaxiom name term
:rule-classes rule-classes
:doc doc-string)
</pre>
where <code>name</code> is a new symbolic name (see <a href="NAME.html">name</a>), <code>term</code> is a term
intended to be a new axiom, and <code><a href="RULE-CLASSES.html">rule-classes</a></code> and <code><a href="DOC-STRING.html">doc-string</a></code> are as
described in the corresponding <a href="DOCUMENTATION.html">documentation</a> topics . The two keyword
arguments are optional. If <code>:</code><code><a href="RULE-CLASSES.html">rule-classes</a></code> is not supplied, the list
<code>(:rewrite)</code> is used; if you wish the axiom to generate no rules,
specify <code>:</code><code><a href="RULE-CLASSES.html">rule-classes</a></code> <code>nil</code>.
<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>
|
