{"entities":{"Q7361840":{"pageid":31521059,"ns":120,"title":"Item:Q7361840","lastrevid":105369767,"modified":"2026-10-07T13:38:39Z","type":"item","id":"Q7361840","labels":{"en":{"language":"en","value":"First-Order Terms"}},"descriptions":{"en":{"language":"en","value":"AFP entry First_Order_Terms"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"511659a8f7458c09cc154d1cd809985eba2a370a","datavalue":{"value":"https://isa-afp.org/entries/First_Order_Terms.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361840$CF00062D-583D-4202-984B-22530C023888","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a56c33c49680ed15bf9438494fe87a6286c086fc","datavalue":{"value":{"time":"+2018-02-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361840$99F6AB3C-9A31-47E3-BAFA-314A65C350B9","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7335db8cbac804a8435e80e80636b4dde04d73bd","datavalue":{"value":"Christian Sternagel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361840$4D5E0A92-49E4-48FB-8DD6-F2F8AA9F727F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"3e961f1f2b2e533bd88ffdbcd178bd2ef2813f73","datavalue":{"value":"Ren\u00e9 Thiemann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361840$6A8112CF-BF32-48AF-B225-09B9B78E3E6C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"883f1aa5451d3da7b9d86871079d87cbea93f8e4","datavalue":{"value":{"text":"First-Order Terms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361840$2A24E5E1-AE97-4F8E-A85D-CF9EFAB9ABB7","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8642ed03cde4c94b6674036c24ee445b30d5a8d1","datavalue":{"value":"We formalize basic results on first-order terms, including matching and a first-order unification algorithm, as well as well-foundedness of the subsumption order. This entry is part of the Isabelle Formalization of Rewriting IsaFoR , where first-order terms are omni-present: the unification algorithm is used to certify several confluence and termination techniques, like critical-pair computation and dependency graph approximations; and the subsumption order is a crucial ingredient for completion.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361840$5C949D2E-D796-4BC1-9609-535340090DA4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0aef60bd392ccfb5e82daa98f095917b33d1745","datavalue":{"value":{"entity-type":"item","numeric-id":3183545,"id":"Q3183545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361840$51F425AC-62FA-4B2F-AF39-AC7915BE9882","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":"Q7361840$FA6073F1-1C8C-4606-B8CA-6ABDB010708B","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"bb0293970cb12cb0c0b06315232bb60667277b31","datavalue":{"value":{"entity-type":"item","numeric-id":7361362,"id":"Q7361362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361840$070907D8-F362-4563-ADE2-952F479F7C95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"2df63eaed94b8a24c8331bb134612d6bfc9cb1c0","datavalue":{"value":{"entity-type":"item","numeric-id":7361479,"id":"Q7361479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361840$BA93485A-3805-437F-8030-E2781F856AC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"c7a8f6bee75646b3f0253f9b38a1467a1e90950c","datavalue":{"value":{"entity-type":"item","numeric-id":7361712,"id":"Q7361712"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361840$25949EF5-97D9-453D-A8C0-0EE527B12E1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"0c9c9f0c4eee9c4734b6223c2dd6a0c94c9a6581","datavalue":{"value":{"entity-type":"item","numeric-id":7361085,"id":"Q7361085"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361840$06106120-D9E3-486D-8A7A-3746B504626F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"c8b055357156b513ebffa05abff4ab0fc053c1d6","datavalue":{"value":{"entity-type":"item","numeric-id":7361662,"id":"Q7361662"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361840$5773D41E-85FA-4886-9B9A-FD5D03AB9D34","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"edf8a8949edec3767dd80b6d3acecc92e5d25f1c","datavalue":{"value":{"entity-type":"item","numeric-id":7360818,"id":"Q7360818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361840$DF237F88-3E48-4ABA-B227-72508BF0DE8D","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":"Q7361840$87A17E2B-B826-4E55-8038-83100CF6890B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"First-Order Terms","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/First-Order_Terms"}}}}}