{"entities":{"Q7361032":{"pageid":31518635,"ns":120,"title":"Item:Q7361032","lastrevid":105362459,"modified":"2026-10-07T13:34:13Z","type":"item","id":"Q7361032","labels":{"en":{"language":"en","value":"First-Order Theory of Rewriting"}},"descriptions":{"en":{"language":"en","value":"AFP entry FO_Theory_Rewriting"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"74616ed711577ceb27b1422d273117093c0adf26","datavalue":{"value":"https://isa-afp.org/entries/FO_Theory_Rewriting.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361032$4BDF3B89-693B-4519-8943-053C66F80A0A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b49dc9fca49651caf99815e140828b876b484fdc","datavalue":{"value":{"time":"+2022-02-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361032$CD2955D0-0982-4459-9410-524F170EBE19","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"5b201f8eb56d8a55f3a204c86041c459a75c34ff","datavalue":{"value":"Alexander Lochmann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361032$0437D7EA-9849-497B-9A8A-3D15EA4E6631","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"4773936992e4bab2a9a45e7e94c36b9477a2fce6","datavalue":{"value":"Bertram Felgenhauer","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361032$1785B661-D2CF-43C4-B26A-93C344B1411F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"19e47b2f3c73b40f8a94b6a5868e76d7a6689e44","datavalue":{"value":{"text":"First-Order Theory of Rewriting","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361032$67F0BC73-8B52-4964-A4A8-AAA0FA6697C1","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"2cb7cd8f01c3897b9bcb186fb529b28371245a86","datavalue":{"value":"The first-order theory of rewriting (FORT) is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata technique and an inference system presented in \"Certifying Proofs in the First-Order Theory of Rewriting\". This AFP entry provides a formalization of the underlying decision procedure. Moreover it allows to generate a function that can verify each inference step via the code generation facility of Isabelle/HOL. Additionally it contains the specification of a certificate language (that allows to state proofs in FORT) and a formalized function that allows to verify the validity of the proof. This gives software tool authors, that implement the decision procedure, the possibility to verify their output.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361032$2B40827E-6656-4B52-ABAA-A7B7A3098CE5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"22b7f440e058e0ee22c7a94ee12acfae059d57fc","datavalue":{"value":{"entity-type":"item","numeric-id":5881191,"id":"Q5881191"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361032$8FFCD96C-555A-4C34-927D-DD102B24A8AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18d21f5617c22e77033d0e0a1f68ccfd52aa981b","datavalue":{"value":{"entity-type":"item","numeric-id":2233502,"id":"Q2233502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361032$F56B1C95-DB51-4CF6-8ED2-132DD6153CCE","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":"Q7361032$B812D673-A6F7-4062-8BF5-E9078E54DDF7","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"5b23589eced77217122b2d223cf1e7808fbf0972","datavalue":{"value":{"entity-type":"item","numeric-id":7361682,"id":"Q7361682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361032$85B8B3E5-DA46-4C06-B70A-3561D3332D4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"6a51b297aa92d91e8ee7b8e9ba22b35272808178","datavalue":{"value":{"entity-type":"item","numeric-id":7361314,"id":"Q7361314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361032$9F575B35-AEA7-40A5-A78C-D6F379409C00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"cc10eb56dc44db7cf056c61e68b7b8997e1a8881","datavalue":{"value":{"entity-type":"item","numeric-id":7361685,"id":"Q7361685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361032$6EFDB38C-9DC0-474C-9F21-C26461D5172E","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"73d93a21b0749f7f2c51d7daeb11b162660cd756","datavalue":{"value":{"entity-type":"item","numeric-id":7360784,"id":"Q7360784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361032$49CCF292-30EE-49AD-A583-0978EF61A659","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"0010e22d998484f218097f7f79d7fc22bc7427c6","datavalue":{"value":{"entity-type":"item","numeric-id":7360817,"id":"Q7360817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361032$776F88D7-3A7D-46D1-A6CA-468BEFB70E2D","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":"Q7361032$E52B2C6C-E32B-482A-A9D5-DDBC68DBCF6F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"First-Order Theory of Rewriting","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/First-Order_Theory_of_Rewriting"}}}}}