{"entities":{"Q2710799":{"pageid":2721538,"ns":120,"title":"Item:Q2710799","lastrevid":82802759,"modified":"2026-05-06T22:07:05Z","type":"item","id":"Q2710799","labels":{"en":{"language":"en","value":"The practicality of generating semantic trees for proofs of unsatisfiability"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1592704"}},"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":"Q2710799$83EB6AB7-F1F0-4305-982C-D682D6A98BFD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f4322a55a3902a27f965fce1e9395872034d5ccb","datavalue":{"value":{"text":"The practicality of generating semantic trees for proofs of unsatisfiability","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2710799$65C3DDE9-90A1-4EF2-827C-94BEF86E70AB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2dae84fde9c4e5f35bf15b489be2763b7d647c12","datavalue":{"value":"1001.68513","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2710799$E827E30F-25CB-4D17-B7BC-0270F6AB6332","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4922f03dcf479c459adc10636ee8e57e6725c407","datavalue":{"value":"10.1080/00207169608804524","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2710799$520FA29F-369A-4979-AED7-C273B98858BE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1f8a1cf422dc8a39955e3a7180ef4ce8229538d6","datavalue":{"value":{"entity-type":"item","numeric-id":2710741,"id":"Q2710741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2710799$E3DD7F37-ECBA-4E7A-9F83-CB1D5027943F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2391050808db64b076e4aa1701660fbac53a4b8d","datavalue":{"value":{"time":"+2002-12-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2710799$C7390850-B7D1-4985-8F1B-5947D0323817","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2710799$BF85C62C-B30F-48E8-8672-0AFA58D93809","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2710799$2619D5F9-F742-413F-89A8-AC89928012A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"344f62a15ccd40e690364bd758985e8313f47f4a","datavalue":{"value":"68R10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2710799$47F3234A-F01B-4E74-AB97-7D460C25BDE8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9734dfa55489b9c06751817b877719c5fc912e2f","datavalue":{"value":"1592704","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2710799$5BE72E88-FDC8-45D0-A9C9-2ED5EC887EB7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b28556cc87db6d65020982562b393f6fbdb98277","datavalue":{"value":"Herbrand universe","type":"string"},"datatype":"string"},"type":"statement","id":"Q2710799$47EB48F6-09BD-4D41-A0FE-FB1B0161C103","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0c684c527af3979997ea37dcd232097f7091ef06","datavalue":{"value":"Herbrand base","type":"string"},"datatype":"string"},"type":"statement","id":"Q2710799$72D277E0-C3A1-42F3-A82F-E9A94C37BA62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"588fe7046e7c4fa6cfcf5f49bf7209a89dba37f4","datavalue":{"value":"unsatisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q2710799$156B960E-55D9-4A73-8F46-6441CD737F70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a3f6bce346b13069e2d2d7e7227e186fa6094b35","datavalue":{"value":"Herbrand interpretation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2710799$9A32CEA9-45BF-45B9-A51B-95F6F64139C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a6754bd98df18de6ab517f0136498d33b949b76d","datavalue":{"value":"Herbrand procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q2710799$F89C2E59-BCD4-4094-940E-1A46B7F9DB26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"34faa57811b42c7ef4e4a37c6ce6bdc7e8be0ee8","datavalue":{"value":"semantic trees","type":"string"},"datatype":"string"},"type":"statement","id":"Q2710799$9AAAB3E0-5911-4A2A-99A1-561F66DF6256","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6738e8db0f627d83ecc52a74051aa80dae8b20bd","datavalue":{"value":{"entity-type":"item","numeric-id":1277338,"id":"Q1277338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2710799$E58C9347-E9AE-4D01-AE1B-9A67AC051497","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4147413905ba97d7ea1ec9d0f2b99addf0d474c6","datavalue":{"value":{"entity-type":"item","numeric-id":1354040,"id":"Q1354040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2710799$67282165-E808-4895-B18F-2A4B530F2DF3","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c7bea7b1a95583dcf9c47a48e1f0734187b198c5","datavalue":{"value":{"entity-type":"item","numeric-id":14474,"id":"Q14474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2710799$267FF06D-4D95-4495-880C-16F281CCACC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c845b927c7c8299e3e10848fbe9373f51ae3559b","datavalue":{"value":{"entity-type":"item","numeric-id":13461,"id":"Q13461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2710799$AE178897-7213-48A4-BD08-B0AB69103202","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":"Q2710799$8A7EB253-9A26-4719-B717-B7C2821A604C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5290d98404659b1ab7a57d3b0bc9f513f36924f8","datavalue":{"value":"https://doi.org/10.1080/00207169608804524","type":"string"},"datatype":"url"},"type":"statement","id":"Q2710799$93617E64-306B-4891-BF53-2EB4482791F0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e90087f1058222753f7506bf631d122724cf143a","datavalue":{"value":"W2079454194","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2710799$CA393909-1478-4251-9421-3FC2A61C29B1","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f20e02bb907f90cb22a0a676f448fd7139f7410","datavalue":{"value":{"entity-type":"item","numeric-id":2547495,"id":"Q2547495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2710799$60DA924F-8B62-4899-B6A9-5157CCD6A5D8","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":"Q2710799$460B0E58-785B-4C22-B8B9-772B93759890","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1aa9e8bb4ef37ec285d6c238c3f5aa5ed5c9a38","datavalue":{"value":{"entity-type":"item","numeric-id":4139711,"id":"Q4139711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2710799$8A738362-4156-4067-9A04-EE20C9E36762","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"914ef8719678eb4ee59028ba65b4741c8aa1bc8e","datavalue":{"value":{"entity-type":"item","numeric-id":4124327,"id":"Q4124327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2710799$8A4FB31D-E836-44CF-9773-E690CC796F80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"21418fbc0bf456401f76f2d9527e7e25f956bfbf","datavalue":{"value":{"entity-type":"item","numeric-id":2551695,"id":"Q2551695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2710799$56DA7EFC-0AF4-4759-84F8-A42836A28ECD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2710799$4972BB39-F8E1-4D7F-8C30-CA1C879FEAB1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The practicality of generating semantic trees for proofs of unsatisfiability","badges":[]}}}}}