Plogic

Propositional logic evaluator and pattern transformer written in Rust. Plogic evaluates logic expressions in a REPL (Read, Execute, Print, Loop) environment and generates every truth table necessary to derive the final truth table result. Another use-case of Plogic is to define and apply pattern rules to transform a expression into another expression. This is a common operation in proof systems. Plogic is a very basic version of a proof system.

This project is build purely out of recreational and educational purposes.

Getting started

To build the binary executable, cargo is required alongside the Rust installation.

$ git clone https://github.com/Janko-dev/plogic.git
$ cd plogic
$ cargo build --release

Go to target/release/ to find the plogic.exe (on windows). Run the executable to enter the REPL environment.

$ cargo run --release
Welcome to the REPL of Plogic.
Usage:
   ----------------------------------------
   | And oprator      |  '&'  | 'and'     |
   | Or oprator       |  '|'  | 'or'      |
   | Not oprator      |  '~'  | 'not'     |
   | Cond oprator     |  '->' | 'implies' |
   | Bi-Cond oprator  | '<->' | 'equiv'   |
   ----------------------------------------
   -----------------------------------------------------------------------
   | Rule       |  ':='  | identifier-name := lhs-pattern = rhs-pattern  |
   | binding    | 'rule' | example:   commutative := p & q = q & p       |
   -----------------------------------------------------------------------
   | Rule       |  '=>'  | inline pattern: A & B => p & q = q & p        |
   | Derivation |        | bound pattern : A & B => commutative          |
   -----------------------------------------------------------------------
   - help:   usage info
   - ans:    previous answer
   - toggle: toggle between (T/F) and (1/0) in truth tables
   - quit:   exit repl
> p & q
---------------------
[ q ] [ p ] [ p & q ]
|---| |---| |-------|
| 0 | | 0 | |   0   |
| 1 | | 0 | |   0   |
| 0 | | 1 | |   0   |
| 1 | | 1 | |   1   |
---------------------
>

Grammar

The following grammar describes the parsing strategy to build the abstract syntax tree. It is noteworthy to mention that the usual mathematical symbols for the operators are not used. Instead, the operators come from the bitwise operators found in various programming languages and optional keywords which may be used for the sake of convenience. The table below shows what each operator means.

Operator	Meaning
`&` or `and`	The and-operator which says that both left-hand side and right-hand side should evaluate to true, for the result to equal true as well.
`\|` or `or`	The or-operator which says that either or both left-hand side and right-hand side should evaluate to true, for the result to equal true as well.
`~` or `not`	The negation-operator flips true to false and false to true.
`->` or `implies`	The conditional implication-operator only evaluates to false when the left-hand side is true and the right-hand side is false, otherwise the result is true.
`<->` or `equiv`	The biconditional implication-operator only evaluates to true when both left and right hand sides are equal to eachother.

Rule-based pattern matching

Furthermore, to pattern match expressions and transform them into other expressions, the => or rule keyword is used after a valid propositional expression. Thereafter must follow a valid left hand-side expression, then a =, and then a valid right hand-side expression. Example:

A & (B | C) => p & (q | r) = (p & q) | (p & r)

This expression describes the following. The expression A & (B | C) will be matched against the left hand-side after =>, i.e. p & (q | r). Since both have the same pattern, it is a valid match. Thereafter, the right hand-side will be substituted according to the matched symbols in the left hand-side. Therefore, producing the following result:

(A & B) | (A & C)

In the case that the left hand-side did not match the expression, an attempt will be made to match the right hand side instead. The same procedure for pattern matching applies, only in reverse. Now, the right hand-side is matched, then substituted in the left hand-side of the given rule. An example will make this more clear. Consider the 'almost' same expression:

(A & B) | (A & C) => p & (q | r) = (p & q) | (p & r)

Notice that the left hand-side of the rule portion p & (q | r) does not match the sub-expression (A & B) | (A & C). Therefore, the right hand-side will be attempted to match, which produces the result:

A & (B | C)

Aside from using inline rule patterns as demonstrated above, which can get convoluted to type if the given rule pattern is used multiple times, there is also the possibility to bind a rule to an identifier name. Consider the following:

distributive := p & (q | r) = (p & q) | (p & r)

the identifier name distributive is now bound to the pattern given after :=. The pattern identifier can now be used instead. i.e.,

A & (B | C) => distributive

which produces the same result as before, i.e., (A & B) | (A & C).

Expression       = Rule_binding | Rule_apply ;
Rule_binding     = Atom ":=" Bi_conditional "=" Bi_conditional ;
Rule_apply       = Bi_conditional ("=>" Bi_conditional "=" Bi_conditional)? ;
Bi_conditional   = Conditional (("<->") Conditional)* ;
Conditional      = Or (("->") Or)* ;
Or               = And (("|") And)* ;
And              = Negation (("&") Negation)* ;
Negation         = "~" Negation | Primary ;
Primary          = Atom | "(" Bi_conditional ")" ;
Atom             = ["a"-"z" | "A"-"Z"]* ;

More Examples

> A & ~A
-----------------------
[ A ] [ ~A ] [ A & ~A ]
|---| |----| |--------|
| 0 | | 1  | |   0    |
| 1 | | 0  | |   0    |
-----------------------

> (p implies q) and (q implies p) 
-----------------------------------------------------------------------------------
[ q ] [ p ] [ (q -> p) ] [ (p -> q) ] [ q -> p ] [ p -> q ] [ (p -> q) & (q -> p) ]
|---| |---| |----------| |----------| |--------| |--------| |---------------------|
| 0 | | 0 | |    1     | |    1     | |   1    | |   1    | |          1          |
| 1 | | 0 | |    0     | |    1     | |   0    | |   1    | |          0          |
| 0 | | 1 | |    1     | |    0     | |   1    | |   0    | |          0          |
| 1 | | 1 | |    1     | |    1     | |   1    | |   1    | |          1          |
-----------------------------------------------------------------------------------

> A & (B | C) => p & (q | r) = (p & q) | (p & r)
(A & B) | (A & C)
> ans
-----------------------------------------------------------
[ C ] [ B ] [ A ] [ A & C ] [ A & B ] [ (A & B) | (A & C) ]
|---| |---| |---| |-------| |-------| |-------------------|
| 0 | | 0 | | 0 | |   0   | |   0   | |         0         |
| 0 | | 0 | | 1 | |   0   | |   0   | |         0         |
| 0 | | 1 | | 0 | |   0   | |   0   | |         0         |
| 0 | | 1 | | 1 | |   0   | |   1   | |         1         |
| 1 | | 0 | | 0 | |   0   | |   0   | |         0         |
| 1 | | 0 | | 1 | |   1   | |   0   | |         1         |
| 1 | | 1 | | 0 | |   0   | |   0   | |         0         |
| 1 | | 1 | | 1 | |   1   | |   1   | |         1         |
-----------------------------------------------------------
>

> DeMorgan := ~(p & q) = ~p | ~q      
> ~((a -> b) & ~(b -> c)) => DeMorgan
~(a -> b) | ~~(b -> c)
> toggle
Changed truthtable symbols from '1'/'0' to 'T'/'F'
> ans
-------------------------------------------------------------------------------------------------------------
[ c ] [ b ] [ a ] [ ~(b -> c) ] [ ~(a -> b) ] [ ~~(b -> c) ] [ b -> c ] [ a -> b ] [ ~(a -> b) | ~~(b -> c) ]
|---| |---| |---| |-----------| |-----------| |------------| |--------| |--------| |------------------------|
| F | | F | | F | |     F     | |     F     | |     T      | |   T    | |   T    | |           T            |
| F | | F | | T | |     F     | |     T     | |     T      | |   T    | |   F    | |           T            |
| F | | T | | F | |     T     | |     F     | |     F      | |   F    | |   T    | |           F            |
| F | | T | | T | |     T     | |     F     | |     F      | |   F    | |   T    | |           F            |
| T | | F | | F | |     F     | |     F     | |     T      | |   T    | |   T    | |           T            |
| T | | F | | T | |     F     | |     T     | |     T      | |   T    | |   F    | |           T            |
| T | | T | | F | |     F     | |     F     | |     T      | |   T    | |   T    | |           T            |
| T | | T | | T | |     F     | |     F     | |     T      | |   T    | |   T    | |           T            |
-------------------------------------------------------------------------------------------------------------

CBOR (binary JSON) for Rust with automatic type based decoding and encoding.

THIS PROJECT IS UNMAINTAINED. USE serde_cbor INSTEAD. This crate provides an implementation of RFC 7049, which specifies Concise Binary Object Represe

121 Dec 27, 2022

Generate commit messages using GPT3 based on your changes and commit history.

Commit Generate commit messages using GPT-3 based on your changes and commit history. Install You need Rust and Cargo installed on your machine. See t

40 Jan 3, 2023

🏪 Modern emoji picker popup for desktop, based on Emoji Mart, built with Tauri and Svelte

Emoji Mart desktop popup Modern emoji picker popup app for desktop, based on the amazing Emoji Mart web component. 🍾 Built as a popup: quick invocati

10 Jul 3, 2023

A lending iterator trait based on generic associated types and higher-rank trait bounds

A lending iterator trait based on higher-rank trait bounds (HRTBs) A lending iterator is an iterator which lends mutable borrows to the items it retur

6 Oct 23, 2023

A merkle-based token distributor for the Solana network that allows distributing a combination of unlocked and linearly unlocked tokens.

merkle-distributor A program for distributing tokens efficiently via uploading a Merkle root. Claiming Airdrop via CLI To claim via CLI instead of usi

6 Dec 8, 2023

Scope-based single and multithreaded profiling.

Add quantifiers

Something missing in this iteration is quantifiers. I would like to take a shot at implementing them, but I will probably not get around to it before exams (October-November in the southern hemisphere).

NS Ek sien jy is 'n Nederlander. Hoe goed verstaan jy Afrikaans?

opened by L0uisc 5