Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] specialised proof procedures for source logics


view this post on Zulip 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: Mar 28 2024 at 12:29 UTC