[isabelle] Full vs Henkin Semantics

Is HOL in Isabelle/HOL based on full semantics or Henkin semantics [1]?

If it is full semantics, are there any automated theorem provers based
on Henkin semantics for higher-order or secord-order logic?


[1] http://en.wikipedia.org/wiki/Higher-order_logic

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