Welcome to IDP-Z3’s Reference Manual

This document describes the IDP-Z3 ecosystem for FO(.). Other learning resources include:

• IDP-Z3 by example.

• the FO[.] standard

Feel free to contact us on our Matrix channel if you have any question on this documentation.

Contents:

• Introduction
  • Installation using poetry
  • Installation using pip
  • Installation of idp_engine module
• The FO[·] Language
  • Overview
  • Shebang
  • Vocabulary
    • Types
    • Predicates
    • Functions
    • Variable Declarations
    • Built-in functions
    • Propositions and Constants
    • Include another vocabulary
    • Symbol annotations
    • URIs
  • Theory
    • Mathematical expressions and Terms
    • Sentences and axioms
    • Definitions
    • Annotations
  • Structure
  • Differences with IDP3
• IDP-Z3
  • webIDE
    • Main block
    • idp_engine functions
    • Theory class
  • Command Line Interface
  • Python API
    • IDP class
• Interactive Consultant
  • Display block
  • Environment & Decision
  • Default Structure
  • Alternative Notations
    • cDMN
    • Feature Modeling
• Explanations
  • Type checking
  • Type inference in quantifications
  • Recursive datatypes
• Appendix: IDP-Z3 internal reference
  • Architecture
    • Web clients
    • Read The Docs, Homepage
    • IDP-Z3 server
    • IDP-Z3 engine
    • Z3
    • Appendix: Dependencies and Licences
  • Datamodel
  • idp_engine module
    • idp_engine.Parse
    • idp_engine.Expression
    • idp_engine.Annotate
    • idp_engine.Interpret
    • idp_engine.Simplify
    • idp_engine.Propagate
    • idp_engine.idp_to_Z3
    • idp_engine.Theory
    • idp_engine.Assignments
    • idp_engine.Run
    • idp_engine.utils
  • idp_web_server module
    • idp_web_server.Inferences
    • idp_web_server.IO
    • idp_web_server.rest
    • idp_web_server.State
• Appendix: Syntax summary
• Index

Indices and tables

• Index

• Search Page