← Back to Project | Installation → | Architecture →
Docs/
├── README.md # This file - documentation hub and navigation
├── installation/ # Setup and configuration guides
│ ├── README.md # Installation documentation hub
│ ├── BASIC_INSTALLATION.md # Standard pip installation
│ ├── GETTING_STARTED.md # First steps after installation
│ ├── TROUBLESHOOTING.md # Platform-specific solutions
│ ├── VIRTUAL_ENVIRONMENTS.md # Virtual environment setup
│ ├── JUPYTER_SETUP.md # Jupyter notebook configuration
│ ├── DEVELOPER_SETUP.md # Development environment setup
│ ├── USING_GIT.md # Git tutorial and workflow
│ ├── CLAUDE_CODE.md # AI-assisted development
│ └── CLAUDE_TEMPLATE.md # Claude Code templates
├── architecture/ # Programmatic semantics framework
│ ├── README.md # Architecture documentation hub
│ ├── PIPELINE.md # System design and integration
│ ├── BUILDER.md # Pipeline orchestration
│ ├── SYNTACTIC.md # AST conversion pipeline
│ ├── SEMANTICS.md # Constraint generation
│ ├── MODELS.md # SMT solving and interpretation
│ ├── ITERATE.md # Model iteration system
│ ├── SETTINGS.md # Configuration hierarchy
│ ├── OUTPUT.md # Output generation
│ ├── THEORY_LIB.md # Theory framework
│ ├── JUPYTER.md # Interactive tools
│ └── UTILS.md # Shared utilities
├── usage/ # Practical usage guides
│ ├── README.md # Usage documentation hub
│ ├── WORKFLOW.md # Comprehensive workflows
│ ├── PROJECT.md # Project setup guide
│ ├── EXAMPLES.md # Example file structure
│ ├── SETTINGS.md # Settings configuration
│ ├── OPERATORS.md # Operator definitions
│ ├── SEMANTICS.md # Testing semantic constraints
│ ├── OUTPUT.md # Output formats
│ └── TOOLS.md # Advanced tools and comparison
├── theory/ # Theoretical foundations
│ ├── README.md # Theory documentation hub
│ ├── HYPERINTENSIONAL.md # Hyperintensional logic
│ ├── Z3_BACKGROUND.md # SMT solver background
│ ├── REFERENCES.md # Academic bibliography
│ └── IMPLEMENTATION.md # Implementation insights
└── maintenance/ # Standards and best practices
├── README.md # Maintenance documentation hub
├── AUDIENCE.md # Audience guidelines
├── VERSION_CONTROL.md # Git best practices
├── quality/ # Documentation quality control
│ ├── README.md # Quality standards hub
│ ├── DOCUMENTATION_STANDARDS.md # Documentation principles
│ ├── README_STANDARDS.md # README requirements
│ └── CONTINUOUS_IMPROVEMENT.md # Quality improvement processes
└── templates/ # Documentation templates
├── README.md # Template usage guide
├── README_TEMPLATE.md # Basic README template
├── THEORY_README.md # Theory README template
└── SUBTHEORY_README.md # Subtheory README template
This directory serves as the comprehensive documentation hub for the ModelChecker framework, providing user guides, research documentation, and theoretical background. The documentation is organized into 5 major categories: installation and setup, programmatic semantics architecture, practical usage workflows, theoretical foundations, and maintenance standards.
The documentation follows an interdisciplinary approach, making computational logic accessible to researchers from diverse backgrounds including logic, linguistics, computer science, and AI. Each section is designed to be self-contained while providing clear navigation to related topics, enabling readers to find exactly what they need without navigating through unrelated content.
For technical implementation details, including API documentation, development workflows, and architecture specifics, see the Developer Documentation. This separation ensures that users focused on applying ModelChecker can find practical guides here, while developers working on the framework itself have dedicated technical resources.
Get started with a simple validity check:
# Install ModelChecker
pip install model-checker# Create example file: modus_ponens.py
from model_checker.theory_lib.logos import get_theory
theory = get_theory()
# Modus ponens example
MP_premises = ["A", "A \\rightarrow B"]
MP_conclusions = ["B"]
MP_settings = {
'N': 3, # Max atomic propositions
'expectation': False # False = expect theorem
}
MP_example = [
MP_premises,
MP_conclusions,
MP_settings
]
example_range = {"MP": MP_example}
semantic_theories = {"logos": theory}The methodology transforms logical arguments through stages:
Input: premises=["A"], conclusions=["B"], settings={'N': 3}
1. Syntax parsing → AST construction
2. Semantic interpretation → Z3 constraints
3. Model finding → Satisfying assignment
4. Result interpretation → Countermodel display
The ModelChecker can accommodate a wide range of different semantic theories, providing a methodology for implementing semantic theories programmatically as well as a TheoryLib consisting of different semantic theories that have been implemented so far.
To bring out the contrast between theories with different expressive powers, consider the following sentences:
# Hyperintensional semantics reveals three levels of equivalence:
# Consider logically equivalent formulas with different structure
# 1. Material equivalence (same truth value in actual world):
"(A \\leftrightarrow (A \\wedge (A \\vee B)))"
# - Logos: Theorem
# 2. Necessary equivalence (same truth value in all possibilities):
"\\Box(A \\leftrightarrow (A \\wedge (A \\vee B)))"
# - Logos: Theorem
# 3. Propositional identity (express the same hyperintensional proposition):
"(A \\equiv (A \\wedge (A \\vee B)))"
# - Logos: Finds countermodels (different subject-matters)For hands-on examples, see Getting Started.
Comprehensive installation and setup guides covering 6 scenarios from basic pip installation to full development environments. Includes platform-specific troubleshooting, virtual environment management, and Jupyter configuration. See installation/README.md for complete setup documentation.
Programmatic semantics framework documentation explaining how ModelChecker transforms logical formulas into executable semantic programs. Covers system architecture, pipeline orchestration, syntax processing, constraint generation, model finding, and iteration strategies. See architecture/README.md for the complete methodology guide.
Practical usage guides for working with ModelChecker, including comprehensive workflows for all features and specialized theory comparison techniques. Covers command-line usage, debugging, performance optimization, and integration patterns. See usage/README.md for practical workflows.
Theoretical foundations and research context including hyperintensional logic, truthmaker semantics, SMT solving background, and implementation insights. Provides the academic grounding for ModelChecker's approach. See theory/README.md for theoretical documentation.
Standards and best practices ensuring consistency across the codebase. Covers comprehensive development standards, documentation quality control, and template resources. Includes specialized quality standards directory and documentation templates for consistent structure. See maintenance/README.md for all standards.
- Installation Guide - Choose your setup path
- Getting Started - First steps tutorial
- Basic Workflows - Running examples
- Theoretical Foundations - Academic background
- Architecture Overview - Programmatic semantics
- ModelChecker Tools - Advanced features and comparison
- Constraint Testing - Proving properties by absence
- Developer Setup - Contributing environment
- Technical Docs - Implementation details
- Maintenance Standards - Code quality guides
- Quality Standards - Documentation quality control
- Documentation Templates - Standardized README structures
- 5 major documentation categories with dedicated README hubs
- 30+ detailed guides covering all aspects of ModelChecker
- Quality-controlled documentation with comprehensive standards and templates
- Interdisciplinary approach serving diverse academic backgrounds
- Clear navigation with consistent structure and cross-references
- Installation options from basic to advanced development setups
- Practical workflows for common tasks and debugging
- Theory comparison guides for research applications
- Getting started tutorials for immediate productivity
- Theoretical grounding in truthmaker semantics
- Academic bibliography with proper citations
- Implementation insights bridging theory and practice
- Architecture documentation for understanding the approach
- Technical Documentation - Development and API docs
- Theory Library - Implementations
- Main Package - ModelChecker overview
- GitHub Repository - Source code
- PyPI Package - Python package
- Z3 Prover - SMT solver documentation