Home / Glossary / Axiom

Strictly speaking, an axiom is one of a set of fundamental formulas that one starts with to prove theorems by deduction. In Cyc, the axioms are the formulas that have been locally asserted into the Cyc KB. Cyc axioms are well-formed formulas, since the system won’t let you add formulas to Cyc that are not well-formed. However, not all well-formed Cyc formulas are axioms, since not all of them are actually in the KB. And some of the formulas in the KB are not, strictly speaking, axioms, since they were added to the KB via inference, instead of being locally asserted.

In informal usage, though, Cyclists don’t always adhere to the strict meaning of “axiom”, and may refer to a formula they are considering adding to the KB or have recently removed from the KB as an axiom.