{"entities":{"Q7361336":{"pageid":31519547,"ns":120,"title":"Item:Q7361336","lastrevid":105365033,"modified":"2026-10-07T13:35:33Z","type":"item","id":"Q7361336","labels":{"en":{"language":"en","value":"A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover"}},"descriptions":{"en":{"language":"en","value":"AFP entry Functional_Ordered_Resolution_Prover"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7620f4aac6a6509783d6a5dfa8994dbfc8a68d21","datavalue":{"value":"https://isa-afp.org/entries/Functional_Ordered_Resolution_Prover.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361336$E315B26E-B8A7-46EC-9532-1415C0CA8A8C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f1e747551cea3e18facbfe25be36852721064ef5","datavalue":{"value":{"time":"+2018-11-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361336$9178DB3B-3312-426E-B7EE-24F2D4452EBA","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"f19e42813e41b1b694ee6662dce0e445e8e41f4b","datavalue":{"value":"Anders Schlichtkrull","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361336$D4DE8404-4E9B-48CC-AE7F-D1C2FE02B5F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"d593b6f197721b1ecf9f17d8e5bbb2bb5a1f7f8a","datavalue":{"value":"Jasmin Christian Blanchette","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361336$D85EE372-FEFA-45DA-B783-B664E17EEDA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2500aa80beaafa12dfa4ab6c7d8363674f762e6e","datavalue":{"value":"Dmitriy Traytel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361336$6E1E78D7-861D-479F-AE32-A89E2CF6F93B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1deb73afd5a9aecc04b278f12dee3d0093586999","datavalue":{"value":{"text":"A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361336$5CFBFA09-0E42-4C9A-9F0E-77A21107DEF3","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e08b1d162a4af804c87594dc6f4120bd09937eb7","datavalue":{"value":"This Isabelle/HOL formalization refines the abstract ordered resolution prover presented in Section 4.3 of Bachmair and Ganzinger's \"Resolution Theorem Proving\" chapter in the Handbook of Automated Reasoning . The result is a functional implementation of a first-order prover.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361336$24E5E3F1-BF35-4E99-943B-5EBFAFCCADDF","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":"Q7361336$D428E1B8-4000-4A0F-A309-42BB2A209D30","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"6d228da4bce2fba997fec5a975b2ba853633b29e","datavalue":{"value":{"entity-type":"item","numeric-id":7361840,"id":"Q7361840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361336$75B2999A-B35A-4A34-997E-2700ADCBC855","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"5d2b901a95ee4a9674d7709b6eab726a2a838e0f","datavalue":{"value":{"entity-type":"item","numeric-id":7361077,"id":"Q7361077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361336$29B5CA6A-3519-4D40-B123-9A6C22C72187","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"cd0c9d6eaf2232ef6bd24acb440211c3c1735214","datavalue":{"value":{"entity-type":"item","numeric-id":7361192,"id":"Q7361192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361336$91411910-8C20-4FF9-A835-60F7B2936C04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"8f0f13c41ff97fc90cd117120ced19e3dd24a1b3","datavalue":{"value":{"entity-type":"item","numeric-id":7361305,"id":"Q7361305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361336$2D9836EF-1ACA-4277-8AFD-3F4CDE7B4D4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"890c0c4a61156b4e729dc9fcff8e39e1971a8f5e","datavalue":{"value":{"entity-type":"item","numeric-id":7361686,"id":"Q7361686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361336$BF48063B-4E46-4CE3-AA40-2A0BA744233A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"505db3695b4bfab8c374d45d12041cac811b0acf","datavalue":{"value":{"entity-type":"item","numeric-id":7361268,"id":"Q7361268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361336$4D05F072-D626-490C-9C37-FA13AA16CB56","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":"Q7361336$DA7D9F5D-EF01-4F0E-9242-FC2656FF3954","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"fd4ac40fec1edeb460421a77e059cfe2df479821","datavalue":{"value":{"entity-type":"item","numeric-id":7360812,"id":"Q7360812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361336$22429453-9DBC-42D4-B5B2-297EE7C65390","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":"Q7361336$A8DABF0A-283E-4E2D-8A05-FCAEE492ABB1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Verified_Functional_Implementation_of_Bachmair_and_Ganzinger%27s_Ordered_Resolution_Prover"}}}}}