search

Deducteam / zenon_modulo

First-order automated theorem prover based on the tableau method
Other
12 stars 6 forks source link

Add support for $ite_t and $ite_f #16

Closed cstolze closed 11 months ago

cstolze commented 12 months ago

The operator $ite_f(a,b,c) has been implemented as ((not a or b) and (a or c)) at the parser level, and the operator $ite_t(a,b,c) has been implemented as a polymorphic expression, similarly to the equality operator. However, I have not implemented a semantics for $ite_t.