search

melvic-ybanez / lohika

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

Alpha-conversion #24

Closed melvic-ybanez closed 2 months ago

melvic-ybanez commented 2 months ago

In the process of converting formulas into PNF, we need to ensure that all quantifications have unique variable names to preserve the original meaning of the formulas. To achieve that, any duplicated variable name must be renamed. Hence, alpha-conversion is required.

melvic-ybanez commented 2 months ago

Closed by 62415834d75d5734eb85df15aa5e2c62e634e895, 5352e6f0bf7aec5c76e77a5a0cf892755dc982e1, and b481011f2ddbb82507945e7d3a83601166230f72