[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?

Thanks,
Andrew

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




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