Patent Document ID: 9489221
Application ID: 12146373
Patent Flag: 1

Claim One:
1. In a computing environment comprising at least one processor and one computer-readable storage media, a method for inferring formula patterns in an arbitrary formula using mixed second-order pattern matching, the method comprising: accessing the arbitrary formula; instantiating each first-order place-holder in the arbitrary formula by one or more sub-formulas or one or more sub-terms; checking that multiple instantiations of each sub-term or each sub-formula coincide when instantiating a same pattern variable; instantiating each second-order place-holder in the arbitrary formula by making one or more substitutions for one or more functions and for one or more relation symbols in the arbitrary formula, wherein: the instantiation of each second-order place-holder in the arbitrary formula is performed by (i) compiling the arbitrary formula into an arbitrary code sequence and (ii) matching the arbitrary code sequence against matching formulas and matching relation symbols, wherein the matching formulas and the matching relation symbols are compiled into matching code sequences, and wherein the matching code sequences are maintained as entries in a matching database as first formulas with first-order place-holders, second formulas with second-order place holders, and first-order patterns; and one of the one or more substitutions for at least one function of the one or more functions in the arbitrary formula includes a pseudo-function comprising: an associated second-order place-holder representing a function symbol of the at least one function; a first variable of the pseudo-function that is equal to an arity of the at least one function; and a second variable of the pseudo-function that is equal to an offset of a next available register, wherein the next available register is a first register of an array of registers that is reserved for storing a plurality of arguments associated with the at least one function; identifying a bound identifier in the arbitrary formula; and associating a first occurrence of the bound identifier in the arbitrary formula with a permutation, the permutation comprising a sub-term that resides on an index of the first register, the sub-term being in a scope of weak second-order variables or function symbols.