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
