Major Section: EVENTS

WARNING: We strongly recommend that you not add axioms. If at all
possible you should use `defun`

or `mutual-recursion`

to define new
concepts recursively or use `encapsulate`

to constrain them
constructively. If your goal is to defer a proof by using a
top-down style, consider using `skip-proofs`

; 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.

Example: (defaxiom sbar (equal t nil) :rule-classes nil :doc ":Doc-Section ...") General Form: (defaxiom name term :rule-classes rule-classes :doc doc-string)where

`name`

is a new symbolic name (see name), `term`

is a term
intended to be a new axiom, and `rule-classes`

and `doc-string`

are as
described in the corresponding documentation topics . The two keyword
arguments are optional. If `:`

`rule-classes`

is not supplied, the list
`(:rewrite)`

is used; if you wish the axiom to generate no rules,
specify `:`

`rule-classes`

`nil`

.