[isabelle] specialised proof procedures for source logics



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

- Gergely




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.