{"entities":{"Q1264000":{"pageid":1274750,"ns":120,"title":"Item:Q1264000","lastrevid":68331984,"modified":"2026-04-12T22:59:29Z","type":"item","id":"Q1264000","labels":{"en":{"language":"en","value":"On an unsatisfiability-satisfiability prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4128430"}},"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":"Q1264000$CABC8C30-7458-40D1-BF1B-6ABDE7E0BD59","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6bfee93032bcc473eea7ea94422b3c809745b93d","datavalue":{"value":{"text":"On an unsatisfiability-satisfiability prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1264000$B02142A2-2EF9-4DBA-85B5-082940E25510","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ef3e922aa007324890cce33b5423af6069bbfb94","datavalue":{"value":"0688.68084","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1264000$3908E10B-5AF8-4C89-BE10-54F1541DD20D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bcd45a4a11a18ec79b2f91ff2c2aaa69dc855b8b","datavalue":{"value":{"entity-type":"item","numeric-id":1229707,"id":"Q1229707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264000$EE728E91-40F3-4F5A-A08B-105CC157716A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"c56c33ef3e883cbe56a171d93462893c540cb008","datavalue":{"value":{"entity-type":"item","numeric-id":174692,"id":"Q174692"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264000$C6DCA12E-2C2B-4084-AEF2-C4292B1F4DBC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7211ad5ca16eb0d22cd0051fff3d0f3af254ceb6","datavalue":{"value":{"time":"+1989-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1264000$88CF281E-0993-490C-9B01-1DF47146AEC3","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a1a9ea4ca4c407d539159dccec32c8364effee60","datavalue":{"value":"Summary: We study a new unsatisfiability-satisfiability prover and its basic properties. Our main results, besides the presentation of our prover, is to show that our procedure always terminates if a given set of clauses is satisfiable in some finite domain. The unsatisfiability checking of our procedure is as strong as the existing complete proof procedures, so we examine the strength of the satisfiability checking part of our procedure. We give an unsatisfiability-satisfiability prover, and show its soundness that is for any unsatisfiable set of clauses the procedure says that it is unsatisfiable, and if the procedure says that the set of clauses is satisfiable, then it is in fact satisfiable. We show that for a given set of clauses assumed to be satisfiable in a simple theory of Herbrand universe, the procedure terminates saying it is satisfiable. We show that for a given set of clauses assumed to be satisfiable in some finite domain, the procedure terminates saying it is satisfiable.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1264000$0E5F6324-894B-453B-9B17-0E2B1D979DF5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1264000$EC6C7E3D-14A2-4349-BE3C-1795A541081D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1264000$67570F51-8A64-4D97-AFF8-C46EDC71DD2F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"186d8c648a31725e9198916f60b097e2ed7462c0","datavalue":{"value":"4128430","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1264000$635F95F1-E958-4840-8C7B-76D4E5B8A187","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1264000$224263EC-E453-4404-BC36-628F76487CF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b28556cc87db6d65020982562b393f6fbdb98277","datavalue":{"value":"Herbrand universe","type":"string"},"datatype":"string"},"type":"statement","id":"Q1264000$17E5DECA-3245-4F17-94A2-E2D4F89C7F6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"10e9843bdfd97faff89897222039f623857f8d12","datavalue":{"value":"finite domain","type":"string"},"datatype":"string"},"type":"statement","id":"Q1264000$FB50A071-8C80-4F3A-B1BB-C1DB0813DA9A","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":"Q1264000$06252BC2-F327-420E-9721-CF1849FC9983","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fe21b26728aa9400aea287981ba35c6123b28b23","datavalue":{"value":"https://doi.org/10.2977/prims/1195173764","type":"string"},"datatype":"url"},"type":"statement","id":"Q1264000$A083F598-ADFA-4F00-ACC2-570DD4A92F7A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8c99bb18e2869a0d4bd15266191b13f9e658fe71","datavalue":{"value":"W1998238433","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1264000$E4C12B09-F437-4B60-B29E-46CEA8087428","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ed4e2b73edd0e2661ebb75822eda29ecb9eb63a","datavalue":{"value":{"entity-type":"item","numeric-id":3906484,"id":"Q3906484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264000$E8534589-7C3A-4B28-8911-5ED8A3F82BA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a85302529ae8048931d942accdfde415f39d0d59","datavalue":{"value":{"entity-type":"item","numeric-id":2554609,"id":"Q2554609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264000$BCAB841E-3CB9-4B14-B7E5-C31AE066410B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264000$E9D1FAE4-E85B-4799-9038-CD489D3A84EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f28f9060d78a8d509e4a96bdf7415308caae8e22","datavalue":{"value":{"entity-type":"item","numeric-id":1060857,"id":"Q1060857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264000$183C40E6-2CE6-4616-937F-24B4667FAACE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73bc9edb29d7084829a8f07a4cc246fa1116d182","datavalue":{"value":{"entity-type":"item","numeric-id":3832537,"id":"Q3832537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264000$32A02BEC-2D51-4EC9-A881-3190D0B6B002","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd37a31c5ce9eb3310a3d2861b39c852af91e8aa","datavalue":{"value":{"entity-type":"item","numeric-id":1149799,"id":"Q1149799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264000$FF0E4783-6C86-4675-A286-FAF7AA368E4E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f86eeb3137c09d3eeed742bc79fbf0f4ac4c5f22","datavalue":{"value":"10.2977/PRIMS/1195173764","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1264000$3E5BBB45-117C-487A-9CA6-1357F2A4AA51","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"93a8ca07be360716357edb360f85a7ed768dbd8e","datavalue":{"value":{"entity-type":"item","numeric-id":3817018,"id":"Q3817018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0cd203970d91a884ec8e9f3d81d5487d4572305","datavalue":{"value":{"amount":"+0.7447799444198608","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":"Q1264000$A3A5AAE4-4D6F-4783-A784-27B4C973EDFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e366a6ae1ffcd391788169251187e485eed88162","datavalue":{"value":{"entity-type":"item","numeric-id":5687274,"id":"Q5687274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ec8af7a03925a2dffca890bb0b00589a1f463c0","datavalue":{"value":{"amount":"+0.7269574999809265","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":"Q1264000$FEB54AE8-4D1B-4900-A483-8612640759E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4b900bbab9d3bf018c3327657c79e4778ce79563","datavalue":{"value":{"entity-type":"item","numeric-id":2723442,"id":"Q2723442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ec8af7a03925a2dffca890bb0b00589a1f463c0","datavalue":{"value":{"amount":"+0.7269574999809265","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":"Q1264000$35554DE1-075E-48EE-88C0-84864682BAEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18eadd68ef3a275c2b540e7d1f3026fdd79c63b3","datavalue":{"value":{"entity-type":"item","numeric-id":4036286,"id":"Q4036286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a95a214b6d9a3269b99f39a84b5c69f0ea3ba46","datavalue":{"value":{"amount":"+0.7267839908599854","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":"Q1264000$43ECFC82-578C-49AE-93A8-4A67DB44D646","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b3a65100382352596d03b0e27223ea49104cd169","datavalue":{"value":{"entity-type":"item","numeric-id":3564034,"id":"Q3564034"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d612d1afa70748956f7aca5cee1fdd3f1c347a9","datavalue":{"value":{"amount":"+0.7251551747322083","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":"Q1264000$4E58C8AD-374D-46FD-8092-74BCA62910D9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On an unsatisfiability-satisfiability prover","badges":[]}}}}}