Email Gateway (Aug 19 2022 at 11:32): Email Gateway (Aug 19 2022 at 11:32):From: Gergely Buday <gbuday@gmail.com>
Hi,
I'm taking a look on reducing nonclassical logic to higher order logic
for which theorem provers are available. In the paper "Encoding
two-valued nonclassical logics" [1], the authors say
"Predicate logic theorem provers which are highly optimized for the
particular fragment of predicate logic which is the target of the
translation are not available."
As this was written more than a decade ago, it can be that some
progress has been made concerning predicate logic. Could someone point
to relevant literature?
And, are there research results for higher order logic as a target logic?
[1] Ohlbach, Nonnengart, de Rijke, Gabbay: Encoding two-valued
nonclassical logics, in: Handbook of Automated Reasoning
Last updated: Nov 21 2024 at 12:39 UTC