{"entities":{"Q1364068":{"pageid":1374807,"ns":120,"title":"Item:Q1364068","lastrevid":70976556,"modified":"2026-04-13T18:38:27Z","type":"item","id":"Q1364068","labels":{"en":{"language":"en","value":"Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1051105"}},"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":"Q1364068$7EC21CE7-E27C-4620-A0F2-E12172625D77","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8aeb53605382e2c0aa9af4b56a03225338287358","datavalue":{"value":{"text":"Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1364068$C034A3EA-45D1-47C4-BD05-30D361BDE3D9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c75ee89409c56f2c1b4757bc1624b7bdb0e7fb66","datavalue":{"value":"0881.68109","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1364068$36C45404-4D0C-41F5-A41A-7B3633E01AAB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9ba50de7c30a75e28a243757063c7e0a6bc19c33","datavalue":{"value":"10.1007/BF02366511","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1364068$77797854-652F-4A92-AE02-B12D62354E9F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"99695ddadc16515df4f5c4d7c88447e67fef4ae5","datavalue":{"value":{"entity-type":"item","numeric-id":1364067,"id":"Q1364067"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1364068$50AFC3B8-BCBF-4F88-A605-FA1C550A027E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a9e0106a8247e4bf7b79a4b47524f15fadc8ba6c","datavalue":{"value":{"entity-type":"item","numeric-id":1127548,"id":"Q1127548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1364068$008CAA73-1DD6-4768-8393-4FFD46E656DD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1b023419c56b9969f2d98b08637e9b0af86a936b","datavalue":{"value":{"entity-type":"item","numeric-id":199816,"id":"Q199816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1364068$59B8D331-2A83-4B24-9E53-4AE335AEF120","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"53ca32303030cbcdd57a20141335cf713f9048cc","datavalue":{"value":{"time":"+1997-10-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1364068$730B4E2B-F834-49F0-A9FC-91B3D3F54090","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1364068$F1A3918A-63E1-456E-B267-A78D0A1C8F8F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2710db4eabf59d30a57a7343dd796c4a7ab6eeed","datavalue":{"value":"1051105","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1364068$76D48AF6-46C6-455B-B071-EB24A3D08B0A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1364068$C48A8F25-7E12-429D-8092-442927BCB8FF","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":"Q1364068$CB6D1896-642D-4FD2-800A-D877D1FA2F67","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ef75b4b5ae4f1119c1ac9bfdcf91039dbf37c93","datavalue":{"value":{"entity-type":"item","numeric-id":3829089,"id":"Q3829089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1364068$E477315C-0699-43D7-9EC7-7336F1DE3CF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1a8c1250dbca5a1914c2e0ccc1c1670d1eb9d18","datavalue":{"value":{"entity-type":"item","numeric-id":1157923,"id":"Q1157923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1364068$128FD5B5-7AA8-42B9-A4D1-3B8EC209D36D","rank":"normal"},{"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":"Q1364068$9BFD8577-7AF7-4E4A-BF23-A9D1E7FD7EAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"82285947ecd1d65d80e17696025cdf5ddb799be6","datavalue":{"value":{"entity-type":"item","numeric-id":3922205,"id":"Q3922205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1364068$FF551C7E-C0C3-423E-97FE-2A5BFF375E5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"280442ce105b23ca3597e15fa2038c58314d7165","datavalue":{"value":{"entity-type":"item","numeric-id":1845619,"id":"Q1845619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1364068$D74891C7-2349-48FC-99E9-C968163069C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e13e861216dffa98af4b697b1dfac9157d7d3662","datavalue":{"value":{"entity-type":"item","numeric-id":5616170,"id":"Q5616170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1364068$A7E02928-D9C3-4B42-8DEE-A46A4A40A153","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":"Q1364068$88F0AF1B-FE5B-438E-944C-6A5EC87F63BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"836ad2a04f82225da478ca9f694f5cd99360b315","datavalue":{"value":{"entity-type":"item","numeric-id":4198056,"id":"Q4198056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1364068$87987E3E-174D-4D92-AD5B-0E7C47813477","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3dc42060a3c506d7dd41e1120918b2d738a6ec64","datavalue":{"value":{"entity-type":"item","numeric-id":1601835,"id":"Q1601835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d5e9b3c115bba1e53031290c5ccfe06817f8c70a","datavalue":{"value":{"amount":"+0.7754887938499451","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":"Q1364068$D91859E8-B387-4A3A-AF67-6A3AE0153433","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b69d387c210ac0b16fdb7d240cff647e1a0c7b9f","datavalue":{"value":{"entity-type":"item","numeric-id":2737323,"id":"Q2737323"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c6262d70e259eb351db49b32a8809a385931a930","datavalue":{"value":{"amount":"+0.7721161842346191","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":"Q1364068$95A4F9E0-A829-47F5-B25A-4ADFF04BC3DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f62d3c74f1452c00e4d697b29b4b03afa7c01b35","datavalue":{"value":{"entity-type":"item","numeric-id":865629,"id":"Q865629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"55ec8d37c1f11347a2355cb7c19585b312518ae9","datavalue":{"value":{"amount":"+0.7664384841918945","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":"Q1364068$7081149A-6887-434A-8AFE-2283945F3CBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3be59899f1c5070152f1be6bf1cc78a0b2b15c08","datavalue":{"value":{"entity-type":"item","numeric-id":3484382,"id":"Q3484382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c6927300fd60ef9258ae9e925fd7085668e48127","datavalue":{"value":{"amount":"+0.7571572065353394","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":"Q1364068$1B684134-045D-491A-A95D-355C7AD2D520","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e3d791142e1e65a80dacca3a17722b4ad0e5718b","datavalue":{"value":{"entity-type":"item","numeric-id":3696551,"id":"Q3696551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c699af5ffef7b909dd4f59dcc8e6f234382e36c3","datavalue":{"value":{"amount":"+0.7544772028923035","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":"Q1364068$D9A7FC58-3CDF-4E7B-ADE5-C91F58450FFB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Combining_formal_derivation_search_procedures_and_natural_theorem_proving_techniques_in_an_automated_theorem_proving_system"}}}}}