melvic-ybanez / lohika

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

Investigate: Support for other forms of "Logical Queries" #16

Open melvic-ybanez opened 2 months ago

melvic-ybanez commented 2 months ago

Right now, Lohika only supports proof generation. Maybe we should add support for other Logical Tasks such as equivalence checks, CNF conversions, CNF checks. For instance if the input is of the form P == Q instead of P |= Q, then Lohika should interpret it as an equivalence check task, as opposed to proof generation.