search

melvic-ybanez / lohika

A Proof Generator for Entailments and Tautologies in First-order Logic
MIT License
37 stars 1 forks source link

Absorption Laws #7

Open melvic-ybanez opened 3 months ago

melvic-ybanez commented 3 months ago

P & (P | Q) == P

Note: We don't need to handle P | (P & Q) since it will be handled by the distributive and idempotent laws.

melvic-ybanez commented 2 months ago

Apply this during resolution rather than CNF conversion to preserve information