{"entities":{"Q688572":{"pageid":690421,"ns":120,"title":"Item:Q688572","lastrevid":63494463,"modified":"2026-04-11T13:33:03Z","type":"item","id":"Q688572","labels":{"en":{"language":"en","value":"An extension of the Boyer-Moore theorem prover to support first-order quantification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 444947"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688572$A2C748BD-A798-41F1-B6AF-9EF66E87FD9F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9e780df36685b011a14acf4bcecb125554ba0b08","datavalue":{"value":{"text":"An extension of the Boyer-Moore theorem prover to support first-order quantification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q688572$89767540-B762-4F16-AA21-B3B197FC2562","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b0cf190991302ea096e05093db784e8a4213923d","datavalue":{"value":"0784.68076","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q688572$0BEE57D5-88DF-4941-94E2-F05AAFB9ADDB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fffa79cfd485b228dc4dd3b914a551034cd6feec","datavalue":{"value":"10.1007/BF00245295","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q688572$F1D51D6A-0587-4C2A-8D44-1B75606EF274","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6bbab2ea230ef82cf7d72bee404dd827d5aaeed","datavalue":{"value":{"entity-type":"item","numeric-id":230814,"id":"Q230814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688572$62C9F5A6-36A7-4C10-9ADB-26D576ACCC88","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688572$9812AC19-9A4E-43C7-8297-87256EF07E3D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"00b02a93155106df3387b19c38bc0ac0db89fb82","datavalue":{"value":{"time":"+1994-01-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q688572$F826D63A-3569-4F2D-9930-86A7CFF9E941","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q688572$0FE988C2-8F13-4F4B-977A-F7671D68D1C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"abca938afd309309893053e8ee4f51374fed9de6","datavalue":{"value":"03C07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q688572$8267ED39-E0A2-4C49-9C57-C3FDA87FA1C9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f8c0c8e632f5a53db7dce9404c1b55f03b409b02","datavalue":{"value":"444947","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q688572$E1757F24-672A-45D1-AA9D-1D37AEAC0DB4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"67935c9745e86097c5a009e8bb47d5846729f37a","datavalue":{"value":"Boyer-Moore theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q688572$3BF1A344-DEC4-4625-AC5D-77332C549DDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3cb6d27fde1e3214c7492516628c363d07c12966","datavalue":{"value":"NQTHM","type":"string"},"datatype":"string"},"type":"statement","id":"Q688572$41E86554-C79C-4420-A488-D4989AA0AE5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7566a487b7a6d997819c54c956e3b15079f4b2f9","datavalue":{"value":"Skolemization quantifiers","type":"string"},"datatype":"string"},"type":"statement","id":"Q688572$B9C1A640-2227-41B3-867E-6E62F4FD59C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"38313993633a0611a2805d0e7911de9bcc0083c4","datavalue":{"value":"first-order quantification","type":"string"},"datatype":"string"},"type":"statement","id":"Q688572$EF7DCE1D-BFDA-488D-904A-16FD079270AF","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688572$5E3D0453-23CA-4DD3-B5D3-7B30C6F0D831","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688572$07B8E780-48D3-47CE-8C47-F6A9AA2B73E8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d829c8fbc70990cde1a42595818dc98639789f5","datavalue":{"value":{"entity-type":"item","numeric-id":915498,"id":"Q915498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688572$ADCC9230-9AE2-48BB-B6EB-85374DE2F10E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"283b457c1aa928df8cba388628638010a8a9e043","datavalue":{"value":{"entity-type":"item","numeric-id":4016540,"id":"Q4016540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688572$C408D9F4-1751-4E61-A170-68D015D5DE50","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dbf175ca02fbfe4698f3e33445ec7cdc416b1c24","datavalue":{"value":{"entity-type":"item","numeric-id":5477663,"id":"Q5477663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c6a548c4aac0a9c16a1c811e33ae469ab579f46f","datavalue":{"value":{"amount":"+0.7403098940849304","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q688572$3C37D5DC-9020-4289-A05D-178629CEC992","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"abf898fcd85aa2a37555a4d59abfad3eac2a5c21","datavalue":{"value":{"entity-type":"item","numeric-id":1107510,"id":"Q1107510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4658b459537f92f20f9749961b80f4fab138ff37","datavalue":{"value":{"amount":"+0.7367417216300964","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q688572$64868A22-6F3D-4438-940D-1F743CE717D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fbd5d69562f578d634c455a50b951c3cba745c07","datavalue":{"value":{"entity-type":"item","numeric-id":3773394,"id":"Q3773394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97f18f1b02924438de142094f3cb124ea8dd4d8d","datavalue":{"value":{"amount":"+0.7326228022575378","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q688572$A3ED4FDE-1927-4128-A41E-77411948C903","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"880184504bd47d4aab173f44873bb04dbe6f5cfc","datavalue":{"value":{"entity-type":"item","numeric-id":1309243,"id":"Q1309243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b38dd4effb7e54d1669e35f5be6a4967a8793b54","datavalue":{"value":{"amount":"+0.7263939380645752","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q688572$4B8427DC-E93D-4826-B182-4C662ACFC1A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3cda481b541398e1a99f4b5d3ef12a328b1ce13e","datavalue":{"value":{"entity-type":"item","numeric-id":6488518,"id":"Q6488518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6fc245250e40328e441a5557fc2839d326f34c2e","datavalue":{"value":{"amount":"+0.7189979553222656","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q688572$52AFD007-0F72-4720-A764-DD069DC12178","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An extension of the Boyer-Moore theorem prover to support first-order quantification","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_extension_of_the_Boyer-Moore_theorem_prover_to_support_first-order_quantification"}}}}}