As Michael said, higher order is all over the place, even if first order reasoning is commonplace. One of my favourite higher order statements is the following encapsulation of Skolemization:
SKOLEM_THM; val it = |- ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x): thm Konrad. On Wed, Nov 18, 2015 at 8:23 PM, Michael Norrish < michael.norr...@nicta.com.au> wrote: > Some of the definitions are higher-order. For example, the universal > quantifier has to be higher order because it's a function that takes a > predicate as an argument. > > Even functions like MAP are higher-order because they take functions as > arguments. Often metis is capable of proving useful facts about MAP > because 1) there's a well-known translation that turns higher-order > problems into first-order ones (which metis uses if it has to), or 2) the > goal mentioning MAP is fundamentally first-order anyway. For example, the > theorem > > |- MAP f (l1 ++ l2) = MAP f l1 ++ MAP f l2 > > is first order, and this may be the only property needed to prove the goal. > > Michael > > > On 19 Nov 2015, at 12:14, shengyu shen <shengyus...@icloud.com> wrote: > > > > Dear all: > > > > HOL is a higher order logic theorem prover, while most of the time, we > use first order lib such as season and metis, > > > > So where is the higher order? > > > > Shen > > > ------------------------------------------------------------------------------ > > _______________________________________________ > > hol-info mailing list > > hol-info@lists.sourceforge.net > > https://lists.sourceforge.net/lists/listinfo/hol-info > > > ________________________________ > > The information in this e-mail may be confidential and subject to legal > professional privilege and/or copyright. National ICT Australia Limited > accepts no liability for any damage caused by this email or its attachments. > > > ------------------------------------------------------------------------------ > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
