RODIN / Feature Requests / #354 Arithmetic simplification in Generalized Modus Ponens

#354 Arithmetic simplification in Generalized Modus Ponens

Milestone: 3.9

Status: open

Owner: Laurent Voisin

Labels: Event-B Prover (105)

Priority: 5

Updated: 2023-04-11

Created: 2018-09-19

Creator: Laurent Voisin

Private: No

Following to [bugs:#765], improve Generalized Modus Ponens so that it also considers simplified arithmetic expressions when trying to match two predicates. For instance, the predicates x + 1 = 1 and x = 0 shall be recognized as equivalent. In other words, the genMP reasoner should consider arithmetic simplification when building the list of variants of some predicate.

See also [#342] and [#343] for other proposed improvements of this reasoner

Laurent Voisin - 2020-09-11

Group: 3.5 --> 3.6
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Guillaume Verdier - 2021-07-20

Group: 3.6 --> 3.7
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Guillaume Verdier - 2022-05-10

Group: 3.7 --> 3.8
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Guillaume Verdier - 2023-04-11

Group: 3.8 --> 3.9
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Arithmetic simplification in Generalized Modus Ponens

Group

Searches

Help

#354 Arithmetic simplification in Generalized Modus Ponens

Related

Discussion