isopod00 / fo3_to_cor_translation

This project aims to translate First-Order 3-variable (FO3) predicate logic into the Calculus of Relations (CoR).

FO3 to CoR Translation

This project aims to translate First-Order 3-variable (FO3) predicate logic into the Calculus of Relations (CoR).

Contributors: Anthony Brogni ([email protected]) and Sebastiaan J. C. Joosten ([email protected])

This tool currently supports:

-Object representation of FO3 Expressions (including predicates with repeated arguments and formulas with typed arguments)

-Object representation of CoR Expressions (both homogeneous/untyped and heterogeneous/typed)

-Generation of random formulas and automated testing with the z3-solver Python library

-Discovery of simplification rules with the help of Z3

-Simplification of CoR formulas (both homogeneous/untyped and heterogeneous/typed)

Summary of each File

-FO3_Expressions.py: Definitions of FO3 objects

-COR_Expressions.py: Definitions of CoR objects (homogeneous/untyped)

-Typed_COR_Expressions.py: Definitions of heterogeneous/typed CoR objects

-FO3_Translation_Methods.py: Methods for applying the Good, Nice, and Final translation steps

-Typed_FO3_Translation.py: Contains the modified Final translation step for heterogeneous/typed formulas

-Testing.py: Random formula generation and automated testing with the z-3 solver module

-Typed_Testing.py: A modified version of Testing.py for heterogeneous/typed formulas

-Search_For_Simplification_Rules.py: Code for finding all possible simplification rules of a given size

-Generate_Typed_Rules.py: Code for taking our dictionary of homogeneous rules and producing a dictionary of heterogeneous rules

-Simplify.py: Python code generated from the rules in COR_Rules.txt for simplifying homogeneous CoR expressions

-Typed_Simplify.py: Python code generated from the rules in Typed_COR_Rules.txt for simplifying heterogeneous CoR expressions

-List_Methods.py: Helper methods for treating lists as if they were sets