{"entities":{"Q1340966":{"pageid":1351705,"ns":120,"title":"Item:Q1340966","lastrevid":68506671,"modified":"2026-04-13T00:10:11Z","type":"item","id":"Q1340966","labels":{"en":{"language":"en","value":"Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 704960"}},"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":"Q1340966$8EBB8C69-7A3B-4BF0-96C3-BE8173F41892","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3fbb24b2942f248ef5df80571978b7990ea414e2","datavalue":{"value":{"text":"Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1340966$77C2268D-175A-4300-B4D6-C84668014E4D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6a18961f93a803338ee49f1ee32f2e18c4a1d410","datavalue":{"value":"0805.68103","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1340966$F4247F0C-E7E4-42C8-B20B-2AE843B090DD","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6d620cf9ff026f0cfa22e6558dabd1f948af6e39","datavalue":{"value":"10.1007/BF00885766","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1340966$FC11AB9D-C47D-4785-A6D1-C87024D591B5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1f5f8c560f95a3a7e60d41630a8b70745f361623","datavalue":{"value":{"entity-type":"item","numeric-id":528695,"id":"Q528695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$C775A0A4-2B53-42FE-88E6-BB33665CEA57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"af11810e9f7655231439ca333f95de5ae32b176a","datavalue":{"value":{"entity-type":"item","numeric-id":543852,"id":"Q543852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$519ACA80-EBBB-4FC5-9D66-A82AFBF9422C","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":"Q1340966$4ADCBB25-4137-441A-B625-4FEECBB5094B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"89a5af496da52109cb9fd8ee43aa6e112a9ba241","datavalue":{"value":{"time":"+1994-12-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1340966$68198040-74C5-43CF-85FE-E2810307D3EA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1340966$135A80B0-EA9A-4487-8463-24FFD2276C66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1340966$77981173-06AA-4279-B2E2-21132329BDDE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2201a45954ba2bd1ac0a5d51a57ce5f4b7c09967","datavalue":{"value":"704960","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1340966$A6135B62-E296-458C-9D90-8B88EADDDFEA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2e80a7123e4ea6d0418cb24d37b1837f13e3514","datavalue":{"value":"first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1340966$AD9A8E15-5766-4085-B286-AD32D5DC4EC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1340966$E0C49F97-45AB-4F07-8937-7404DF22FBFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"81ae5c95ce5e013c04ef6fd3dbc79bbb37c1221a","datavalue":{"value":"hyperlinks","type":"string"},"datatype":"string"},"type":"statement","id":"Q1340966$6837CE7D-D8FF-4998-901A-C0102CFBA009","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3922eb0b8235fb2b824bcb3eaa0c8d395dbd512","datavalue":{"value":"unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1340966$384094B5-7EBC-46D8-BBBA-E3DE9F6C50B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c233a8a0952a9a0a6f256be4c9271c215c0b1c45","datavalue":{"value":"clause network","type":"string"},"datatype":"string"},"type":"statement","id":"Q1340966$2F27A212-8ADD-4CE2-AE3C-69DA93A99DB0","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"94ff9ef5b8ae6b6a1b8a58993d59fc90a641e302","datavalue":{"value":{"entity-type":"item","numeric-id":19065,"id":"Q19065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$3F264232-115F-47FA-91F8-887076724949","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"33919c41a1ae48620fd8e94aafcb1944f42ea3d2","datavalue":{"value":{"entity-type":"item","numeric-id":31443,"id":"Q31443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$E94F3F33-3102-4BB3-9807-7AFF3A7BF993","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$EAFED3E4-F2B7-4AB5-B397-5A359D0AA2CA","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":"Q1340966$AD3D9638-E592-41E6-9F35-156588E0A4FA","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e857e95d91a8e9f3746c9aca423c534197fa21d","datavalue":{"value":{"entity-type":"item","numeric-id":1238434,"id":"Q1238434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$C02AE0A5-AE18-465D-9161-F691EAD85E31","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":"Q1340966$C19CC84A-580B-42A8-A2BF-F9F94838C81A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$B716C853-F839-4001-B2EF-5E9B37B5B7C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3322157bf6a01189b1807437698fe608048635ac","datavalue":{"value":{"entity-type":"item","numeric-id":4167597,"id":"Q4167597"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$9D87CE88-70B4-46DA-BB2C-0896F385F301","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88fba5a1fdfac74b8e0dcefe0e56f5b10792486d","datavalue":{"value":{"entity-type":"item","numeric-id":688547,"id":"Q688547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$5030BA7A-14EF-4733-BA06-F610950CF484","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da0678074516c9f8798777e6a10ea9c0403c8e8b","datavalue":{"value":{"entity-type":"item","numeric-id":1337680,"id":"Q1337680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$C012117F-F0FD-4DB4-A93E-E92432B5D890","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":"Q1340966$BADC9F8C-A740-4724-9B3C-DC1CAB39CDCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26e765697dc730e487db4a5421dc5ddcece8b423","datavalue":{"value":{"entity-type":"item","numeric-id":1819949,"id":"Q1819949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$72A249E1-6CB5-4EB0-8BC1-79E6491E6CE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7add01291c95ebcb031afac6fc8c8b1659115c10","datavalue":{"value":{"entity-type":"item","numeric-id":1229761,"id":"Q1229761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$3717FD21-5FAC-4CE5-9616-2008606AEF5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1fa8e099c59f8b6819b5b09b786ac872f2d64b8","datavalue":{"value":{"entity-type":"item","numeric-id":688554,"id":"Q688554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$3788E0D3-9687-4E58-AD16-431412AADF12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5587664e371fa7cdb52e3b1329f22cf9fcff022","datavalue":{"value":{"entity-type":"item","numeric-id":1101242,"id":"Q1101242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$595024E0-6BC4-470A-88DE-9E0488931BD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0001ddf29143e230db9061e7c9cfd72aed8db985","datavalue":{"value":{"entity-type":"item","numeric-id":1170894,"id":"Q1170894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$30E56A89-E715-44DA-A5BD-801AAA127062","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"008723b33cb14bbda59226503d753d137dc6f8ef","datavalue":{"value":{"entity-type":"item","numeric-id":1098330,"id":"Q1098330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$ACEA68C7-5F03-485D-8D0F-ACD24BE6A099","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"adbfa02ab4b7e0bb252f5a5604936a94deac79e9","datavalue":{"value":{"entity-type":"item","numeric-id":3847756,"id":"Q3847756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$66DB08AB-D14C-4FCE-8D9D-3A5DB1403D4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03b5ec7b36ab9f9a9396a2be7f7246c57825af23","datavalue":{"value":{"entity-type":"item","numeric-id":3742689,"id":"Q3742689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$16C0605D-2B8C-43E6-8A19-104ACCBDF094","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ab938ba3d2bb1de7d34dc0f9166735f59a48b21","datavalue":{"value":{"entity-type":"item","numeric-id":1114446,"id":"Q1114446"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$3493E645-56B2-4DE0-95DC-9AFD04FEC7C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c5b09e879fc9e6d166a18cb26ec583e2bf401aa","datavalue":{"value":{"entity-type":"item","numeric-id":1272614,"id":"Q1272614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340966$4121A630-A1F0-47BF-B6FB-A2D1094A0F89","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6d74deb86168d9ac8d9413d92c16d6610686ae23","datavalue":{"value":"https://doi.org/10.1007/bf00885766","type":"string"},"datatype":"url"},"type":"statement","id":"Q1340966$17F93B43-613F-490B-86CE-762F0BB32076","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0fee73ab9f261b5294cd6bdafcb474ba9881c39f","datavalue":{"value":"W1994344807","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1340966$33212359-55D0-47A7-A152-97737311A769","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9e6901df0d59a017c054fa969f1e65edc3a3eb1c","datavalue":{"value":{"entity-type":"item","numeric-id":688547,"id":"Q688547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"156581de0e432657bb1dc1b90e931ac2884857cd","datavalue":{"value":{"amount":"+0.8348649740219116","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":"Q1340966$E432D1C1-7591-4D9A-9821-C6DAD96C6EA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1977ce75e4c66a6e986ece8bd137815f9305537","datavalue":{"value":{"entity-type":"item","numeric-id":4345253,"id":"Q4345253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7c18d609391bfb313d9566e13d9d5d04f4f3f0ee","datavalue":{"value":{"amount":"+0.8304094672203064","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":"Q1340966$32C04561-95F3-4EC8-98B6-0461A1A59A09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"875cc4f73fb74be10087e96ba425671d4de768ef","datavalue":{"value":{"entity-type":"item","numeric-id":1595925,"id":"Q1595925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b74dd6092cefbf7abd173c01b71269c538908154","datavalue":{"value":{"amount":"+0.7844721078872681","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":"Q1340966$421A0F24-5D2F-40C3-ACD1-BBE71C0924B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b31e39c392ede8b11c1ca113b79fb83a462765c","datavalue":{"value":{"entity-type":"item","numeric-id":5210771,"id":"Q5210771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1c2219853862f3bf0cb85ea9b86fe5d650d4c512","datavalue":{"value":{"amount":"+0.7767994403839111","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":"Q1340966$60EF98E0-5F73-48B5-BFAD-40EF091438A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3328acb14c381645dbb1f9eb31b744a4a34bbbc0","datavalue":{"value":{"entity-type":"item","numeric-id":5210762,"id":"Q5210762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"94fa17583f452299893a4eefa1d7a8eb280c86f8","datavalue":{"value":{"amount":"+0.7652155756950378","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":"Q1340966$688CB325-4E66-4A33-A1FE-12617B2ABA44","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Improving_the_efficiency_of_a_hyperlinking-based_theorem_prover_by_incremental_evaluation_with_network_structures"}}}}}