first order logic definition

IRI: https://spec.industrialontologies.org/ontology/annotation/firstOrderLogicDefinition

Defined In: https://spec.industrialontologies.org/ontology/core/meta/AnnotationVocabulary/

Type: Annotation Property

SubProperty Of: logic definition

Definition

logic definition that expresses the axioms of a class or an object property in first order logic

The First Order Logic Definition annotation is comprised of the (complete) necessary and sufficient conditions.

This annotation is Required for each non-primitive (aka non-axiomatic) class (i.e. unary relation) of a published IOF OWL ontology. This is the most authoritative and comprehensive definition of an IOF element.
IOF Common Logic ontologies do not require this annotation, but if included it must be logically equivalent to the Common Logic definition.
A primitive (aka axiomatic) term will not have a First Order Logic definition in either an OWL or Common Logic IOF ontology.
There should be at most one First Order Logic definition.
The specific symbols to be used for existential and universal quantification along with those for conjunction, disjunction, negation, conditional (i.e. if-then), and equivalence will be those commonly used in the mathematical formulas and statements.
Conjunction - ∧; Disjunction - ∨; Negation - ¬; Existential Quantification - ∃; Universal Quantification - ∀; Conditional - →; Equivalence - ↔; Left/Right Parentheses - (,); Left/Right Brackets - {,}.

An example of a First Order Logic definition for ‘Product’ might be (again bearing in mind the natural language terms appearing should be regarded as symbols in the IOF signature):
Continuant(x) ∧ ¬(SpecificallyDependentContinuant(x) ∨ Person(x) ∨ Organization(x)) ∧ ∃r (ProductRole(r) ∧ hasRole(x, r))