{"entities":{"Q7361010":{"pageid":31518569,"ns":120,"title":"Item:Q7361010","lastrevid":105362393,"modified":"2026-10-07T13:34:12Z","type":"item","id":"Q7361010","labels":{"en":{"language":"en","value":"Unification Utilities for Isabelle/ML"}},"descriptions":{"en":{"language":"en","value":"AFP entry ML_Unification"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4224327775c3eac0fc331647bdfdf20667de04d1","datavalue":{"value":"https://isa-afp.org/entries/ML_Unification.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361010$5B29D1EE-1D91-426E-BB62-5AC5D43D6A65","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b8511310b812d9d4a7e586ca3d9e1dbbb6532cd6","datavalue":{"value":{"time":"+2023-09-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361010$2D22A4C5-6121-45B9-95A3-B7C4BC434EBA","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"1dc1799f4552dd027370c421d2790c94fad994fa","datavalue":{"value":"Kevin Kappelmann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361010$3948B76A-FC42-4CA4-B70A-E5333B6FA781","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3f284022d37230cbe2f300e030f286d020443752","datavalue":{"value":{"text":"Unification Utilities for Isabelle/ML","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361010$A9719556-6160-4629-89B9-507C6BD9C774","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"d921732a5d84676bf9d2548ac50a7f64c601a714","datavalue":{"value":"This article provides various unification utilities for Isabelle/ML, most prominently: Proof-producing first-order and higher-order pattern E-unification and E-matching. While unifiers in Isabelle/ML only consider the $\\alpha\\beta\\eta$-equational theory of the $\\lambda$-calculus, unifiers in this article may take an extra background theory, in the form of an equational prover, into account. For example, the unification problem $n + 1 \\equiv {}?m + Suc\\; 0$ may be solved by providing a prover for the background theory $\\forall n.\\ n + 1 \\equiv n + Suc\\; 0$. Tactics, methods, and attributes with adjustable unifiers (e.g. resolution, fact, assumption, OF). A generalisation of unification hints . Unification hints are a flexible extension for unifiers. Among other things, they can be used for reflective tactics, to provide canonical unification instances, or to simply strengthen the background theory of a unifier in a controlled manner. Simplifier integration for E-unifiers. Practical combinations of unification algorithms, e.g. a combination of first-order and higher-order pattern unification. A hierarchical logger for Isabelle/ML, including per logger configurations with log levels, output channels, message filters. While this entry works with every object logic, some extra setup for Isabelle/HOL and application examples are provided. All unifiers are tested with SpecCheck .","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361010$60F00262-7C27-4CD9-AEE2-E5E6CBA513C6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5f64d57050206512889a218305d67a8f65e3f09","datavalue":{"value":{"entity-type":"item","numeric-id":3183522,"id":"Q3183522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361010$DEC934D7-AE27-4E81-A037-41A97E70BCCD","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361010$AF2DC381-11B3-490D-917F-4D98C59F1668","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"35972e4d852b9a97437a6c555f7480f3e52c8876","datavalue":{"value":{"entity-type":"item","numeric-id":7361511,"id":"Q7361511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361010$9C8288B9-A57E-4AB9-8998-116B3DB8C13D","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"7a918ca57cbef7417c708001c9499e7e295238c0","datavalue":{"value":{"entity-type":"item","numeric-id":7360836,"id":"Q7360836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361010$4E4A2847-267D-4B51-A0DF-84C109F6A98C","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361010$C630C989-FFEF-4C10-B9A3-64675D7C14D9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Unification Utilities for Isabelle/ML","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Unification_Utilities_for_Isabelle/ML"}}}}}