|
|
|---|
|
|
|
|---|
Add an axiom
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 proving a formula that is, logically speaking, a theorem of the current theory, then consider using skip-proofs instead. One such case is the use of a top-down style, as per the discussion on ``Top-Down Proof'' in Section B.1.2 of ``Computer-Aided Reasoning: An Approach.'' Note that adding new axioms may frequently render the logic inconsistent!
Example: (defaxiom sbar (equal t nil) :rule-classes nil) General Form: (defaxiom name term :rule-classes rule-classes)
where