SoleLogics
Welcome to the documentation for SoleLogics.jl, a Julia package for computational logic. To let you better orient yourself while understanding SoleLogics' structure, each chapter will begin with a little summary of what you are going to learn, in the form of small type-hierarchy trees that will grow during your reading journey. To see a complete map of SoleLogics.jl types and structures, please refer to Complete Exports Map.
Feature Summary
SoleLogics.jl allows manipulation of:
- Syntax tokens (e.g., atoms, logical constants (e.g., operators and truth values), etc.);
- Alphabets & context-free logical grammars (e.g., normal forms);
- Algebras (e.g., crisp, fuzzy, many-valued);
- Logics (e.g., propositional, (multi)modal);
- Formulas (e.g., syntax trees, DNFs, CNFs): random generation, parsing, minimization;
- Interpretations (e.g., propositional assignments, Kripke structures);
- Algorithms for evaluating the truth of a formula on an interpretation (model checking);
- Interfaces to Z3, for evaluating the validity/satisfiability of a propositional formula.
Installation
To install SoleLogics.jl, use the Julia package manager:
using Pkg
Pkg.add("SoleLogics")About
SoleLogics.jl lays the logical foundations for Sole.jl, an open-source framework for symbolic machine learning, originally designed for machine learning based on modal logics (see Eduard I. Stan's PhD thesis 'Foundations of Modal Symbolic Learning' here).
More on Sole:
The package is developed by the ACLAI Lab @ University of Ferrara.
Complete Types Hierarchy Map
Here is a map of SoleLogics' most important types and structures. Feels overwhelming? Don't worry, if you are not practical with SoleLogics, this is useful to just know what definitions exist and hints at a glance how types are related to each other.