First-Order Logic (FOL) Syntax Guide

This guide explains the syntax rules for writing valid First-Order Logic (FOL) expressions in our system, particularly focusing on compatibility with Basic Formal Ontology (BFO) terms.
Supported Notation Formats

Our system supports two primary notation formats for FOL expressions:

1. BFO Standard Notation (Recommended)

Uses instance_of(x, Class, t) syntax with explicit temporal parameter.

This is the preferred format that allows for temporal reasoning.

forall x, t (instance_of(x, continuant, t) -> exists_at(x, t))
2. Traditional Notation

Uses Class(x) syntax without explicit temporal parameter.

This simplified format is more limited but easier to write.

forall x (Continuant(x) -> exists t (Exists_at(x, t)))
Important: We recommend using the BFO Standard Notation as it provides better compatibility with temporal reasoning and BFO ontologies.
Syntax Elements
Element Symbol Description Example
Universal Quantifier forall For all values of the variable forall x (P(x))
Existential Quantifier exists There exists at least one value of the variable exists x (P(x))
Implication -> If...then... relationship P(x) -> Q(x)
Conjunction & Logical AND P(x) & Q(x)
Disjunction | Logical OR P(x) | Q(x)
Negation - Logical NOT -P(x)
Biconditional <-> If and only if (equivalent to) P(x) <-> Q(x)
Parentheses () Group expressions and establish precedence (P(x) & Q(x)) -> R(x)
Multiple Variable Quantification

For multiple variables in quantifiers, use any of these formats:

  • forall x, t (P(x, t)) - Comma-separated variables (automatically preprocessed)
  • forall x forall t (P(x, t)) - Separate quantifiers
Tip: When using multiple variables in forall x, t format, our system automatically converts it to forall x forall t for compatibility with the parser.
Working with BFO Terms

When writing FOL expressions, you can use any BFO classes and relations. Here are some common BFO terms:

Common BFO Classes
  • entity - The root class of all BFO entities
  • continuant - Entities that persist through time
  • occurrent - Entities that unfold in time
  • independent_continuant - Continuants that don't require bearers
  • material_entity - Physical objects
  • process - Occurrents with temporal parts
Common BFO Relations
  • instance_of - Relates an individual to a class
  • exists_at - Temporal existence of a continuant
  • part_of - Mereological part relation
  • has_part - Inverse of part_of
  • located_in - Spatial location
Note: Our system checks for term compatibility with BFO. Unknown terms will be flagged as "non-BFO terms" in the test results.
CLIF Notation (Common Logic Interchange Format)

CLIF (Common Logic Interchange Format) is a standardized syntax for expressing first-order logic that is more machine-friendly and serves as an ISO standard (ISO/IEC 24707).

CLIF Syntax Basics
  • Uses parenthesized prefix notation
  • Variables start with a question mark or capital letter
  • Quantifiers: (forall (?x) ...) and (exists (?x) ...)
  • Connectives: and, or, not, implies, iff
Example in CLIF
(forall (?x ?t) 
  (if (instance_of ?x continuant ?t) 
      (exists_at ?x ?t)))
Note: While our system currently uses NLTK's parser which follows a more traditional syntax, we plan to add CLIF support in a future update for better interoperability with ontology tools.
Common Errors
Error Example Solution
Missing parentheses forall x P(x) -> Q(x) forall x (P(x) -> Q(x))
Incorrect case for BFO terms instance_of(x, Continuant, t) instance_of(x, continuant, t)
Free variables (not bound by a quantifier) P(x) -> Q(y) forall x (P(x) -> exists y (Q(y)))
Mixed notation formats forall x (Continuant(x) & instance_of(x, entity, t)) Stick to one format: forall x,t (instance_of(x, continuant, t) & instance_of(x, entity, t))
Examples
Valid FOL Expressions
  • forall x,t (instance_of(x, material_entity, t) -> instance_of(x, independent_continuant, t))

    All material entities are independent continuants

  • forall x,t (instance_of(x, process, t) -> instance_of(x, occurrent, t))

    All processes are occurrents

  • forall x,t,u (instance_of(x, continuant, t) & instance_of(x, continuant, u) -> exists_at(x, t) & exists_at(x, u))

    A continuant exists at all times at which it is a continuant

  • forall x,t (instance_of(x, process, t) -> exists y,u (instance_of(y, continuant, u) & participates_in(y, x, u) & part_of(u, t)))

    All processes have at least one continuant participant

Back to Home Test an Expression