{"entities":{"Q1404975":{"pageid":1415715,"ns":120,"title":"Item:Q1404975","lastrevid":68628168,"modified":"2026-04-13T01:01:59Z","type":"item","id":"Q1404975","labels":{"en":{"language":"en","value":"Model building with ordered resolution: Extracting models from saturated clause sets"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1970569"}},"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":"Q1404975$16FF813C-BBCD-4125-8C41-CF3F54CA7089","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cc9ccd684abde08f15e6f4409b7a07c4d2c8e8ad","datavalue":{"value":{"text":"Model building with ordered resolution: Extracting models from saturated clause sets","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1404975$A261C1C8-2DDE-4A47-AE86-964E153006DF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6ca7ef906a762681a3ef937bd7ce514292453032","datavalue":{"value":"1019.03008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404975$80245AA7-2849-42B4-B082-9BD3E9404450","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3ae5936c70f96984f5bf8796f41d95a5b1752acd","datavalue":{"value":"10.1016/S0747-7171(03)00028-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404975$3E70D488-EB8A-4248-B082-955878A11239","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"dbb66b347a8501d3e88bb4fc6db185a6021261a5","datavalue":{"value":{"entity-type":"item","numeric-id":167063,"id":"Q167063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$FAED04AF-2F49-41C2-9B9B-2C0CD06B0B32","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$C2E1DD0C-22F6-4723-8EA3-ECA623B5001A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"988a1f1f38c2f749de54c12ebc5774f827c2b17e","datavalue":{"value":{"time":"+2003-08-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1404975$9BCB8B85-64DD-4C31-9499-6615599FC360","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404975$257D511C-6E1D-43E4-A422-BE342AEC9379","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404975$831E9A85-55CB-442A-AB60-3265C0B27690","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7f6a5506a6b08f2739321d7b6c9caed070f44682","datavalue":{"value":"1970569","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404975$A9DB88DE-812A-4175-B7AE-03DB78EC0F81","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b401ca815ee5cfdb8691f0ebe0ef53103ee246f","datavalue":{"value":"satisfiable clause sets","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404975$E389F5AB-BF07-4AB0-8145-927BA9123B53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"92a8f07d0a3bfabea17b00996461606d492fcacc","datavalue":{"value":"Herbrand model","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404975$1BA948D8-C07D-40FA-B050-13CD25A157C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a84ba88a223d66a255cf717873de1a17d0ae80a1","datavalue":{"value":"tree automaton","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404975$B80E8036-74FB-4FE2-9748-A4D6E63150C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b0133bb82e5a2899974ef5a92a207f1239299d2","datavalue":{"value":"model building","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404975$4141A448-F24E-4223-8725-E2EA996BBFCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7e3cf9bca78e19102e6a3c7dfa3a53aed9896da","datavalue":{"value":"ordered resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404975$9594193E-D4BC-406B-9B8A-BF580FC88CEC","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"70c51cb69cf83ba52d30c7a2c9abf4fc48a6f8a5","datavalue":{"value":{"entity-type":"item","numeric-id":18707,"id":"Q18707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$FCDAE81C-9211-4248-9A09-1864339DB1C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c52067912b0b36fecbbb51adf44957c3c2a0bee","datavalue":{"value":{"entity-type":"item","numeric-id":18797,"id":"Q18797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$F18E4E04-DF2E-460B-8A34-5A7B25AA0FFF","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":"Q1404975$FF321EF1-7CB0-49CC-8F93-59F3F5901345","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"207d1a4f947fa872ea38eb5c749f0304803e02b3","datavalue":{"value":{"entity-type":"item","numeric-id":4282593,"id":"Q4282593"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$25DCCE4E-9455-4563-A900-AC61D825173B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f93041fe6d7db6318dfbd457c9a855fed097172","datavalue":{"value":{"entity-type":"item","numeric-id":4713088,"id":"Q4713088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$98329376-8B38-4E7A-A44E-FC26936D0B60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df4b2cc45597c6adb320160f2d26e8212e854497","datavalue":{"value":{"entity-type":"item","numeric-id":5235250,"id":"Q5235250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$EBE233C5-FC1E-4740-B2DD-416C1D51E36E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a1ee918c464fe7c6c2ebcaf9cb1dfed9d3b10f4","datavalue":{"value":{"entity-type":"item","numeric-id":1581852,"id":"Q1581852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$6ADBDB1F-BBF4-459A-9654-CE029F9DF8B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1867080c0034d7856d12fe14b76198e231d90233","datavalue":{"value":{"entity-type":"item","numeric-id":1198235,"id":"Q1198235"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$5D0567A0-1AD3-4A83-A5B0-BC8E116B5347","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"795bcee8c82c3eb3bbe1d7fbba253638ccbd8a1a","datavalue":{"value":{"entity-type":"item","numeric-id":4314599,"id":"Q4314599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$7BA1C340-F7B9-4553-B6F1-B9D7C7909974","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86db5a5291f3a16cb567c464530440c036bb2b14","datavalue":{"value":{"entity-type":"item","numeric-id":1333268,"id":"Q1333268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$D39FDE30-84AB-4480-B7BB-8727B77C2D8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f241207bb39341afad681685e7fc2b817c7ff774","datavalue":{"value":{"entity-type":"item","numeric-id":1124372,"id":"Q1124372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$4D2817BF-3257-42F7-AA77-1580827E9871","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1272332821781f00780d9c30b66a912b70f4d17","datavalue":{"value":{"entity-type":"item","numeric-id":1854350,"id":"Q1854350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$BC94C3AB-886D-4CD0-A3FC-5EDD9DAD57DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1737e3b82e8627dc5ad82b7bff5fa29662ec6e2f","datavalue":{"value":{"entity-type":"item","numeric-id":4880540,"id":"Q4880540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$0453A74C-9CC9-42A9-9CB8-3DEA82C1CEBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"315e95e4ad8a1c26487d3ff7728ab264483e45ea","datavalue":{"value":{"entity-type":"item","numeric-id":1310269,"id":"Q1310269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$1E06739C-65BB-478B-AC0F-127FBF35E801","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a37da6481d3393a5a430cfe31bbfd3e1bb865a00","datavalue":{"value":{"entity-type":"item","numeric-id":4380444,"id":"Q4380444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$F00CE8B4-EB2E-46B8-98D4-AB7637B2B938","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7dd8d1dd5d31c59ca258af36242eec281a44b582","datavalue":{"value":{"entity-type":"item","numeric-id":3996619,"id":"Q3996619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$555E8635-DAEE-4D28-ADC7-711FF09FE725","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0079b0c7d694a397659be503d6216c85129b1bb1","datavalue":{"value":{"entity-type":"item","numeric-id":3323279,"id":"Q3323279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$40A33D32-9062-40DE-9811-F7108F39B19C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b989303c3f01780ec3752ac791fe5233d16a37b4","datavalue":{"value":{"entity-type":"item","numeric-id":1094888,"id":"Q1094888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$838773FE-66E2-4E11-A099-C72921E6D1D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8755fff25bcbf365d5dd2dfde2f78f833a2371b","datavalue":{"value":{"entity-type":"item","numeric-id":4331764,"id":"Q4331764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$17AB245E-87ED-40F9-8996-1FE9C658DB86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c16bedf88d37c78219926e82b3d7a7a9dee66a31","datavalue":{"value":{"entity-type":"item","numeric-id":3821629,"id":"Q3821629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$1C951829-9B76-45C8-9E36-5EC91F0F0D63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ba991d4e866ef355b82f0e4f0cd0605eb8a7e90","datavalue":{"value":{"entity-type":"item","numeric-id":4362927,"id":"Q4362927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$B8E5E606-039F-4FEA-BEE9-8D5C9D4DF031","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"43494860626967b7048fc0935e6b9a3f87ded8a2","datavalue":{"value":{"entity-type":"item","numeric-id":4349580,"id":"Q4349580"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404975$4B5B3F71-34E9-458D-A450-3A8E7AD6201B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"61566d3f7d09b12a4bef9237af79e3d2ce60a4e2","datavalue":{"value":{"entity-type":"item","numeric-id":1401929,"id":"Q1401929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"30003b0c22d6d364458018d9393a2a89e0956746","datavalue":{"value":{"amount":"+0.8796557784080505","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":"Q1404975$AA199A0E-4E75-4435-9ABC-7F1F07AAA8C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"44469c695c7d19631de7e636f5e7f496493f9406","datavalue":{"value":{"entity-type":"item","numeric-id":4283235,"id":"Q4283235"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f08839bf1414c41f59f4e08b0151354c654695eb","datavalue":{"value":{"amount":"+0.8490681648254395","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":"Q1404975$340C39FA-9387-4009-9B0D-1364ACB5AE71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ed107c0b5f9570cfb041178e0327ee0d9628b0b","datavalue":{"value":{"entity-type":"item","numeric-id":4880540,"id":"Q4880540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"63c6d1e7fedb72bb180a8017b64c3e912a2d0468","datavalue":{"value":{"amount":"+0.8136114478111267","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":"Q1404975$5CB8CD91-33EA-4141-B9E3-30BE0B956907","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b218c4ba3c0ee3527ebaf03168166dd2cb9217ec","datavalue":{"value":{"entity-type":"item","numeric-id":4287493,"id":"Q4287493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b3998748a10db65ec9440b4be5d7d3cf02bbce95","datavalue":{"value":{"amount":"+0.8121213912963867","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":"Q1404975$6CD64920-7204-4239-BCE8-AC54DC28F8DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4f4a6403e32a0fb608b2d78d4fbbcf70b14daa38","datavalue":{"value":{"entity-type":"item","numeric-id":4809059,"id":"Q4809059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d6d3c9dc68e340f20015628d8093528b70f68b62","datavalue":{"value":{"amount":"+0.8062534928321838","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":"Q1404975$E2FC69F3-85E7-4FBB-9511-4103D626AE5E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Model building with ordered resolution: Extracting models from saturated clause sets","badges":[]}}}}}