infeR

infeR is a Rust-based reimplementation of the Inference tool InfOCF-Lib, focusing on foundational components for signature creation, formula manipulation, and syntax splitting of total preorders. This project serves as a robust base for developing advanced algorithms in propositional and preferential logic.

Basic and Advanced Propositional Logic Crate

This Rust crate provides tools for constructing, manipulating, and reasoning with propositional Logic formulas, supporting canonical forms, formula builders, and the Quine-McCluskey algorithm for minimization. It also provides the capabilities to construct total preorders on propositional interpretations and perform syntax splitting on those total preorders.

Due to the increasing size of functionalities in this crate, i have modularized the README.md into each submodule. So while i will give a small high level example of how to use the crate in here, i will give more detailled examples in the according sub-readme.

Overview

The repository is organized into multiple subcrates, each addressing specific aspects of logical inference and manipulation:

• Propositional Logic: Tools for constructing, manipulating, and reasoning with propositional logic formulas. Features include canonical forms, formula builders, and the Quine-McCluskey algorithm for formula minimization.
• Preferential Logic: Utilities for building and managing total preorders, ranking functions, and performing syntax splitting. This subcrate leverages propositional signatures and interpretations to facilitate complex logical operations.
• Logical Builders: A suite of builder utilities for incrementally constructing logical components such as formulas, signatures, variable lists, layer mappings, and total preorders. Ensures robust error handling and ease of use through a fluent API.
• Syntax Splitting: Functionality for decomposing propositional signatures into independent subsets, enabling modular reasoning and analysis within logical frameworks.
• Interfaces: Play with the components using a user-friendly interface of your choice ### WORK IN PROGRESS ###

Features

• Formula Construction: Build complex propositional formulas with logical operators using builder patterns.
• Signature Management: Define and manipulate propositional signatures and variable lists with ergonomic APIs.
• Canonical Forms & Minimization: Generate canonical disjunctive normal forms and minimize formulas using the Quine-McCluskey algorithm.
• Total Preorders: Create and manage total preorders over propositional interpretations, essential for preferential logic.
• Syntax Splitting: Decompose total preorders into independent variable subsets for modular analysis.
• Conditional Compilation: Enable or disable specific functionalities via Cargo features to customize your build.

Conditional Compilation

The project leverages Rust's conditional compilation to provide flexibility and modularity. Optional features can be enabled or disabled in your Cargo.toml to include or exclude specific functionalities:

• preferentials: Integrates the preferential_logic crate, enabling preferential logic capabilities.
• splitting: Enables the syntax_splitting crate for syntax splitting functionalities.
• builders: Enables the logical_builders crate for ergonomically building logical structures.
• interface: Enables the interfaces crate for using the logical structures provided in this project with a convenient web interface, a CLI, or a TUI.

Example Cargo.toml Configuration:

[dependencies]
propositional_logic = "0.0.0"
preferential_logic = { version = "0.0.0", features = ["preferentials"] }
syntax_splitting = { version = "0.0.0", features = ["splitting"] }
logical_builders = "0.0.0"

Getting Started

Prerequesites

• Rust: Install the Rust toolchain from rust-lang.org.
• z3-Solver: Install the z3 Theorem Solver from z3, libclang and export the evironment variable, e.g. for ubuntu:

apt-get update && apt-get install -y clang z3
export LIBCLANG_PATH=/usr/lib/llvm-14/lib/

Installation

1. Clone the repository:

git clone https://codeberg.org/Ypman/infeR.git
cd infeR

2. Build the project in release mode:

cargo b --release

3. Run main.rs:

cargo r

High Level Usage

After setting up the project, you can utilize the various subcrates to build and manipulate logical structures.

Example: Building a Propositional Formula with Syntax Splitting Enabled

To include preferential_logic exclusively:

[dependencies]
propositional_logic = "0.0.0"
logical_builders = { default-features = false, features = ["preferentials"] }

// main.rs
use logical_builders::{SignatureBuilder, LayerMappingBuilder, TotalPreOrderBuilder};

fn main() {
  let signature = SignatureBuilder::new()
    .parse_from_literals("p, q")
    .unwrap()
    .build()
    .unwrap();

  let layer_mapping = LayerMappingBuilder::new()
    .parse_from_literals("0,1,0,2")
    .unwrap()
    .build()
    .unwrap();

  let total_preorder = TotalPreOrderBuilder::new()
    .signature(signature)
    .layer_mapping(layer_mapping)
    .build()
    .unwrap();

  println!("Constructed Total PreOrder: {}", total_preorder); // {(¬p ∧ ¬q)}, {(p ∧ ¬q)}  ≺  {(¬p ∧ q)}  ≺  {(p ∧ q)}
}

Pitfalls

• Signature Compatibility: Ensure that all variables used in formulas are included in the PropositionalSignature. Missing variables can lead to interpretation errors and unexpected behavior.
• Algorithm Complexity: Some algorithms, such as the Quine-McCluskey minimization, can be computationally intensive for formulas with a large number of variables. Optimize usage accordingly.
• Conditional Features: Be mindful of the features enabled in your Cargo.toml. Enabling multiple features might increase compile times and binary sizes.

TODO

• Enhance Documentation: Provide more comprehensive examples and detailed explanations for each subcrate.
• Optimize Algorithms: Improve the performance of computationally intensive algorithms like Quine-McCluskey.
• Expand Syntax Splitting: Implement more advanced syntax splitting techniques to handle complex logical structures.
• Integrate Testing Frameworks: Develop extensive test suites to cover edge cases and ensure robustness.
• Continuous Integration: Set up CI pipelines to automate testing and deployment processes.
• User-Friendly CLI: Develop a command-line interface to interact with the library functionalities more easily.

Contributing

Contributions are welcome! Please ensure:

• New code is well documented.
• Tests cover edge case and expected functionality.

1. Fork the project
2. Create a feature branch: git checkout -b feature/<YourFeature>
3. Commit changes: git commit -m 'Cause of your feature'
4. Push to the branch: git push origin feature/<YourFeature>
5. Open a pull request

License

This project is licensed under the GNU License.

---

Subcrates Overview

Below is a brief overview of each subcrate within the repository. For detailed information, refer to each subcrate's respective README.md.

Propositional Logic

propositional_logic provides tools for constructing, manipulating, and reasoning with propositional logic formulas. Supports canonical forms, formula builders, and minimization algorithms.

Preferential Logic

preferential_logic offers utilities for building and managing total preorders and ranking functions. Facilitates syntax splitting on total preorders to identify independent variable subsets.

Logical Builders

logical_builders provides collection of builder utilities for incrementally constructing logical components such as formulas, signatures, and total preorders. Ensures robust error handling and ease of use.

Syntax Splitting

syntax_splitting enables decomposition of propositional signatures into independent subsets, promoting modular reasoning and analysis within logical frameworks.

Interfaces

interfaces enables playing with logic in ergonomic interfaces like a web interface, a CLI (Command-Line Interface) or a TUI (Terminal-Line Interface). WORK IN PROGRESS!