About FOL-BFO-OWL Tester

Introduction

The FOL-BFO-OWL Tester is a comprehensive web service designed to validate and test First-Order Logic (FOL) expressions against the Basic Formal Ontology (BFO) classes and relations, as well as analyze complete OWL ontologies for consistency, structure, and real-world implications.

This tool helps ontology developers, researchers, and students check if their logical expressions conform to BFO standards, identify potential issues in their formulations, and understand the practical implications of their ontological structures in real-world scenarios.

How It Works
FOL Expression Testing
  1. Enter a FOL Expression: Type or paste your first-order logic expression in the input field.
  2. Test the Expression: Click the "Test Expression" button to analyze your input.
  3. Review Results: The system will parse your expression, check it against BFO classes and relations, and display detailed results.
  4. Fix Issues: If any problems are detected, you can use the provided feedback to refine your expression.
Ontology Analysis
  1. Upload OWL File: Select and upload your OWL ontology file.
  2. Review Analysis: The system automatically analyzes the ontology structure, consistency, and logical relationships.
  3. Explore FOL Premises: View the First-Order Logic premises extracted from your ontology.
  4. Generate Implications: Generate real-world implications based on your ontology's logical structure.
The system checks for:
  • Syntactic validity of FOL expressions
  • Recognition of BFO classes and relations
  • Identification of non-BFO terms
  • Structural issues in expressions
  • Ontology consistency and contradictions
  • Class hierarchies and relationships
  • Axiom validity and completeness
  • Logical implications and entailments
About BFO

The Basic Formal Ontology (BFO) is a top-level ontology designed to support information integration, retrieval, and analysis across diverse scientific domains. BFO serves as a foundation for building domain-specific ontologies in a way that supports interoperability.

BFO divides entities into two main categories:

Continuants
Entities that persist through time while maintaining their identity, even as they undergo different sorts of changes. Examples include objects, qualities, and functions.
Occurrents
Entities that happen or unfold in time. Examples include processes, events, and temporal regions.

For more information about BFO, visit the BFO official website.

Ontology Analysis Features

Our system provides comprehensive ontology analysis capabilities, allowing you to:

Upload and Analyze OWL Files

Upload your OWL (Web Ontology Language) ontology files for comprehensive analysis, including:

  • Class hierarchy extraction
  • Relationship mapping
  • Axiom identification
  • Statistical analysis of ontology structure
  • Consistency checking using reasoners
FOL Premises Extraction

The system extracts First-Order Logic (FOL) premises from your ontology, providing:

  • Translation of OWL axioms to FOL statements
  • Logical interpretation of ontology relations
  • Human-readable descriptions of logical structures
  • Identification of logical patterns and rules
Real-World Implications Generation

Using advanced AI technology, the system generates practical real-world implications from your ontology:

  • AI-powered interpretation of logical structures
  • Generation of concrete scenarios demonstrating logical rules
  • Domain-specific examples of how ontology principles apply
  • Explanations connecting scenarios to specific premises
History and Analysis Tracking

The system maintains a comprehensive history of your ontology analyses:

  • Track all uploaded ontologies
  • Review previous analysis results
  • Compare different versions of ontologies
  • Access previously generated implications
  • Build a knowledge base of ontology insights
Recent Updates

Based on valuable user feedback, we've made the following improvements to the system:

  • Updated to BFO-2020 with expanded class and relation definitions
  • Fixed free variable detection in FOL expressions to identify unbounded variables
  • Created comprehensive FOL syntax guide to help users with both notation formats
  • Improved search functionality and fixed label/ID display for BFO terms
  • Enhanced ID button functionality to automatically use instance_of format
  • Added clearer descriptions of ontology analysis capabilities and BFO integration

Last updated: May 12, 2025

FOL Syntax Guide

When writing First-Order Logic expressions for the tester, use the following syntax:

Logical Operator Symbol Example
Universal Quantifier forall forall x (Human(x) -> Mortal(x))
Existential Quantifier exists exists x (Student(x) & Happy(x))
Conjunction (AND) & Tall(john) & Strong(john)
Disjunction (OR) | Happy(mary) | Sad(mary)
Negation (NOT) ~ ~Raining(today)
Implication -> Wet(grass) -> Rained(recently)
Biconditional <-> Bachelor(x) <-> (Man(x) & ~Married(x))

Variables are typically represented by lowercase letters. Predicates and constants typically start with uppercase letters.

FOL Notation Formats

The system now detects and supports both traditional and BFO standard notation formats for FOL expressions:

Traditional Notation

The legacy format where class membership is represented by applying a predicate to a variable:

Continuant(x)

This format is simpler but less semantically precise for complex BFO ontologies.

Example:

forall x (Human(x) -> Mammal(x))
BFO Standard Notation (Recommended)

The BFO-preferred format that uses the instance_of relation to represent class membership with temporal contexts:

instance_of(x, Continuant, t)

This format is more expressive and handles temporal aspects of BFO entities effectively.

Example:

forall x,t (instance_of(x, Human, t) -> instance_of(x, Mammal, t))
New Feature: The system now automatically detects which format you're using and provides appropriate guidance. While both formats are supported, we recommend using the BFO Standard Notation (instance_of) for more precise and temporally-aware expressions.
Acknowledgments

We would like to express our sincere gratitude to the following individuals for their valuable contributions, feedback, and expertise:

Alan Ruttenberg
BFO and Ontology Expert

Special thanks to Alan Ruttenberg for his invaluable feedback, suggestions, and expertise in improving the BFO integration. His detailed comments and recommendations have significantly enhanced the functionality and accuracy of this tool, particularly in relation to the BFO-2020 implementation and the handling of instance_of relations in FOL expressions.

We also extend our appreciation to the broader ontology community for their ongoing support and feedback that continues to guide the development of this tool.

Project Information

This web service is based on the FOL-BFO-OWL-tester by dkoepsell. The original Python script has been adapted and extended to provide a web interface and API for testing FOL expressions against BFO-OWL guidelines.

Technologies used:

  • Backend: Flask, Python, NLTK, Owlready2, PostgreSQL Database
  • Frontend: HTML5, Bootstrap 5, JavaScript
  • AI Integration: OpenAI API for generating real-world implications
  • Reasoners: HermiT and Pellet for ontology consistency checking