search

Formal-Systems-Laboratory / matching-logic-mm0

Formalisation of Matching Logic in Metamath 0
BSD 3-Clause "New" or "Revised" License
0 stars 1 forks source link

AppCtx axioms missing freshness constraints #20

Closed MirceaS closed 1 year ago

MirceaS commented 1 year ago

https://github.com/MirceaS/matching-logic-mm0/blob/ed1ec0193986bfaee5d6b7e76dbdd3e3db8b8fd2/00-matching-logic.mm0#L200

These 2 axioms need freshness constraints for phi2 and phi1 respectively. The proof system is unsound without them.

@nishantjr

MirceaS commented 1 year ago

Update: Fixed this