search

ctrekker / Deductive.jl

A package for expressing and automatically proving logical statements symbolically in Julia
MIT License
19 stars 2 forks source link

Derived operators #6

Open ctrekker opened 2 years ago

ctrekker commented 2 years ago

Most operators don't need to be defined by an axiom, but rather can be defined in terms of other axiomatic or higher-order operators. For instance, with only a NAND operator definition every other operator in propositional calculus can be defined. In practice it would be easier to have NOT, AND, and OR be the three "axiomatic" operators, even though only NOT and AND are truly necessary (or even just NAND for that matter).

Similarly most of the operators from set theory (exceptions being cardinality and power set) can be defined with set-builder notation, zeroth-order logical operators, and the inclusion operator (∈).

This issue involves formally supporting this kind of derived operator, likely with an abstraction of LogicalOperator.

Other features can be added in a later issue

ctrekker commented 2 years ago

This issue is bigger than I originally thought, so I'll turn this into a project of its own which will constitute the release of version 0.2.0. Considering that efficient reorganization and abstraction of lowered expressions likely has a brute-force time complexity of O(n!) this algorithm alone will take some time to get right.