{"entities":{"Q1098332":{"pageid":1109084,"ns":120,"title":"Item:Q1098332","lastrevid":66126366,"modified":"2026-04-12T07:43:33Z","type":"item","id":"Q1098332","labels":{"en":{"language":"en","value":"Hierarchical deduction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4037273"}},"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":"Q1098332$B8A72134-828B-4013-9C3F-29AC8846D16E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3d2e7f4feffb7fde06a492f4fc21d9a112e9e099","datavalue":{"value":{"text":"Hierarchical deduction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1098332$B4EC941C-F727-4A7D-94E1-9EB785527B3A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d211178e50ed7c97023269981221a2479079acb4","datavalue":{"value":"0636.68120","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1098332$A0C476C2-EC83-4305-95F0-65D2CC977309","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7b70ca4a32884ff4ee142978c5f80056368e3e84","datavalue":{"value":"10.1007/BF00381144","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1098332$73681763-CD33-494B-9D82-64A6CDBAC208","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e794e8ec2d8d673df4039847753be5983884cc10","datavalue":{"value":{"entity-type":"item","numeric-id":1098331,"id":"Q1098331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1098332$8D4EDFD8-C9FE-4C12-BDDE-E076C9B00FCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ac6e57e7cbbcf47c47eab8817c6b7cdfc4fb3e81","datavalue":{"value":{"entity-type":"item","numeric-id":915495,"id":"Q915495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1098332$DF00A32E-CC2C-41AB-97C7-481CC65A4B1F","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":"Q1098332$00A9E531-E198-42D9-A9C8-9AD96951FD38","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5ae48c61eed19d1e1e1f33f9255d5b329362d064","datavalue":{"value":{"time":"+1987-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":"Q1098332$621D1A50-5158-48FA-9118-4B878F19770B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"c68c641171de3dc74198fbc5552758b1031a1a23","datavalue":{"value":"The main contribution of the paper is the goal-oriented hierarchical deduction proof procedure. The procedure proves a theorem by producing not just one but all the acceptable resolvents from the goal clause. There is a set of completeness-preserving refinements to constrain the generation of the irrelevant resolvents.    The paper describes a ground hierarchical deduction procedure applicable to propositional logic and then extends this procedure for first-order logic. A semantically guided hierarchical deduction and a partial set of support strategies are defined as two methods to reduce the search space. The implementation results are included. The authors give an outline of the implemented procedure (HD-Prover) and a list of automatically proved theorems.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1098332$52413990-0C21-4791-A232-4B44096FAD8E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1098332$71A340AD-4D32-4038-A3C2-429DD47E7758","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1098332$0CBEBB6B-8ECD-48CC-9E10-08ABB0A28742","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6d9ddb38b7dc2fe20ec390a357683d217ac7b174","datavalue":{"value":"4037273","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1098332$C0A26039-DF41-41BD-9451-8E1F58FA45A3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1098332$016C8B45-8E24-4E96-9238-376A4FC83FCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"24b43c174201179fab0c965c1796a1970e4f56b2","datavalue":{"value":"goal-oriented deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1098332$387FB2C9-EA5F-4A04-B20A-E6F84AF54081","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"06cfbae9e21a0f8a6153c845b30749ac8d98d983","datavalue":{"value":"resolution unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1098332$F4140F42-BE6D-4E2D-8C89-36810D5B31FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a4fd4daa3631aee7dcfc4a1b2f046d2b04caf47","datavalue":{"value":"hierarchical deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1098332$DBB55071-98BB-415F-97F5-E66963AE39F0","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":"Q1098332$A1846AEC-1BB6-49DC-ABF3-B82448CDF024","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e19bcc8ceeae09bfe2823325d7d61b377dc18bc4","datavalue":{"value":{"entity-type":"item","numeric-id":5597535,"id":"Q5597535"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1098332$0D3FFB28-6F88-4539-84F4-A09DC6AA0E32","rank":"normal"},{"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":"Q1098332$48838D20-83B1-4858-8D78-9C26562C5A15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd4014288d007eedfd81f67ea20b5630186ca313","datavalue":{"value":{"entity-type":"item","numeric-id":3880319,"id":"Q3880319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1098332$D29C421D-860D-48DF-A00B-172B17041983","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":"Q1098332$FC02344F-BEDA-48AB-89A8-E581901115C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2dbf5d4c6cedd5848e03816494729378cde53a8e","datavalue":{"value":{"entity-type":"item","numeric-id":2551698,"id":"Q2551698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1098332$3F36E171-9DCD-4A97-BAD2-B6BB5917B7D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65f72fa731d5ef46f7c8727b7b59f2eaf22c3523","datavalue":{"value":{"entity-type":"item","numeric-id":5544307,"id":"Q5544307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1098332$A234ADA4-6599-41B9-8739-678B48E8D6A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8586c92c4d90a06cb521bef03111f958a597fe2e","datavalue":{"value":{"entity-type":"item","numeric-id":5574714,"id":"Q5574714"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1098332$DDE100AF-EF00-49DC-86B8-5D9F5EE2C392","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a80969bb580420f8ecd201d1cbd7dbd33d4faa0","datavalue":{"value":{"entity-type":"item","numeric-id":4770008,"id":"Q4770008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1098332$2CDB0A0F-67AE-49AC-82E4-AAA8CE718509","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":"Q1098332$91F8E206-B8DB-4B59-814B-0BF23E5FCCDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0aefa01969c4c5ab3568e4445e95ff48e256399","datavalue":{"value":{"entity-type":"item","numeric-id":4095910,"id":"Q4095910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1098332$E69EF0A5-3E6A-4375-BFDF-F4334510A669","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce187d54500a2db26ceae6e0205ecb0b0752213a","datavalue":{"value":{"entity-type":"item","numeric-id":4773313,"id":"Q4773313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1098332$47A4BBB3-C64A-46D4-9FEF-78011AB189F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47bab4f7d1b2661e9a9ca3ddc35e5a57311ad582","datavalue":{"value":{"entity-type":"item","numeric-id":5507985,"id":"Q5507985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1098332$90B2F64D-7DCD-481F-A968-A1F05FE9FC25","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"05e589464eb7aa4ad245c2c7b80c9114dee105d8","datavalue":{"value":"https://doi.org/10.1007/bf00381144","type":"string"},"datatype":"url"},"type":"statement","id":"Q1098332$75FB69A0-FF88-4707-B3DC-8A48DBC0BD4E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d5fedf9fa212437b1727212f75726b9629f5993a","datavalue":{"value":"W2913781829","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1098332$9CA719BF-5AE1-4374-949D-BCC7064EF2F3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b49075e90a95966de1738b235c7e42ffe68077a","datavalue":{"value":{"entity-type":"item","numeric-id":3119162,"id":"Q3119162"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"87edadad309410773c4ad616fc9372ed6a79193d","datavalue":{"value":{"amount":"+0.9047444","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098332$AF28780F-980B-44C0-8ACF-AE9D88465B8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c2eef3bdbda46e4d317c8846893aa96099206e18","datavalue":{"value":{"entity-type":"item","numeric-id":2946680,"id":"Q2946680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5759d74ad2a57bc07aa328ddc4ecdcab2c03d77e","datavalue":{"value":{"amount":"+0.8991096","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098332$27684F1B-B100-420A-8976-BC17F595B54E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c96e279c6310a7975761ec5b6bbb8333f9e8a42","datavalue":{"value":{"entity-type":"item","numeric-id":2410900,"id":"Q2410900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f6b229a364353d4278703777a201be87e55c5d6","datavalue":{"value":{"amount":"+0.89752376","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098332$10EBBEDF-0E6C-40A1-8FB4-792B0BEA0F66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3489a34e2b3742bc93b2bcb5b5928e0f1b67da73","datavalue":{"value":{"entity-type":"item","numeric-id":3533142,"id":"Q3533142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"be0bf7cb0a429bcecf6a5ea7dd4c29d3d9395da6","datavalue":{"value":{"amount":"+0.8909641","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098332$9051D8F7-6BDA-484A-8839-8B1CFEE82632","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6e01417a38bf52a677ff37d08a2853600c75e119","datavalue":{"value":{"entity-type":"item","numeric-id":2301318,"id":"Q2301318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e20638809c063c3bbf2c787ec5ed5b0370e0e5e9","datavalue":{"value":{"amount":"+0.88858813","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098332$837B062E-E388-4C6A-A4B0-F57F16E05D70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2843260133561894537ea85c8f36abd252a38008","datavalue":{"value":{"entity-type":"item","numeric-id":5394615,"id":"Q5394615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"078eda82ad79dff617e17c5824efcb36aea37f11","datavalue":{"value":{"amount":"+0.8812914","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098332$02B52C89-C67A-424D-881E-88DCB8B5D6FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cb0aa6e33b6900b6e526e177272f5d19731fd079","datavalue":{"value":{"entity-type":"item","numeric-id":2333323,"id":"Q2333323"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"67866217830df6bf6a4eebdf2a23b62a43100484","datavalue":{"value":{"amount":"+0.87969697","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098332$98765CE1-2860-4100-81ED-AF86C7A1AA01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dea9003220edf3a4b8dc331eabc919f8e86f5c61","datavalue":{"value":{"entity-type":"item","numeric-id":2958527,"id":"Q2958527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"243304f918e1308bd175f74cf21b3c5a9581fedc","datavalue":{"value":{"amount":"+0.87720156","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098332$6456187A-D7F4-4D97-8A49-4BE265C94959","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"795a3a9265ddade018103da6a26fd286971d0ca4","datavalue":{"value":{"entity-type":"item","numeric-id":4697038,"id":"Q4697038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"80d6c3afca9db4a7384e4d171f221cb2e8cb7ec5","datavalue":{"value":{"amount":"+0.87022126","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098332$DFBE16AB-60D0-4C70-96D0-9DA093018A28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce1bfb88b017f4e4615d2d3b43c1c7343a833bad","datavalue":{"value":{"entity-type":"item","numeric-id":4235216,"id":"Q4235216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f57f96c092898baa507ff31d38ec23f42862f01f","datavalue":{"value":{"amount":"+0.8678535","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098332$98C2506D-F6E6-4988-8E7B-26E5EDFEEA4F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Hierarchical deduction","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Hierarchical_deduction"}}}}}