{"entities":{"Q4720797":{"pageid":6750374,"ns":120,"title":"Item:Q4720797","lastrevid":41889689,"modified":"2025-05-09T11:10:57Z","type":"item","id":"Q4720797","labels":{"en":{"language":"en","value":"Natural deduction as higher-order resolution"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3992944"}},"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":"Q4720797$32C7A559-FD36-4ECF-8CF1-1C5FFE891E47","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"da97e99a1cb52ecd789ba02c4abf394f10fbb700","datavalue":{"value":{"text":"Natural deduction as higher-order resolution","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4720797$C220A26D-2D18-47C3-B064-BEDA133BF6D2","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"39f838d1ef6787ae63d9c71177c29938ad6e7bc0","datavalue":{"value":"0613.68035","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4720797$153CAF6E-230C-464C-B343-08CE7D7982CC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"165a375ef8fea904377411fc62c4db1ea9cdaf82","datavalue":{"value":"10.1016/0743-1066(86)90015-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4720797$D943DE5A-5F61-4012-B88C-B132CC1D97F2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7eb8fbff5b5a1996cd7eff3ff7a29f3a29661a8f","datavalue":{"value":{"entity-type":"item","numeric-id":3030270,"id":"Q3030270"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4720797$6FAF1433-0A58-4669-8ED5-BA507DFFC77E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"63df7153432d81fa42019fcabb076c89649b0b5b","datavalue":{"value":{"time":"+1986-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":"Q4720797$F40EBB00-9902-468F-BD5D-76789EAE3A98","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4720797$A5AD6147-ACD1-46BD-BB66-5ACBCEE7E58C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4720797$92A00F6A-F812-41EA-9265-34C632E3ABB4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"67a419a555df32f86c1117586f636571dcae4825","datavalue":{"value":"3992944","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4720797$2B3BF7FB-ABD2-4C8D-9140-A0D805F8EF1A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q4720797$A3F75B93-EEBC-4062-9792-74B92747A74C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"73f877e2f1bc95df5bf8181b9880837b7bf0c2ee","datavalue":{"value":"interactive theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q4720797$2BFB38FC-8429-430C-B018-C71BACF51A7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"25f88413bb3b2f1f7827c20a3b9cfd81f88e00f1","datavalue":{"value":"Logic of Computable Functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q4720797$77F2E6E4-1FB6-4272-B964-1AD4AFBC7785","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"69dc243280df071bc2603756c6df11ecda1cdb8e","datavalue":{"value":"LCF theorem provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q4720797$CD8B622E-FBF3-4F06-B759-E8CC1A508363","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0e431190495251d75e7d7f973ca704f4139885eb","datavalue":{"value":"Horn clauses","type":"string"},"datatype":"string"},"type":"statement","id":"Q4720797$8416E1A7-92F4-4482-8A3C-5AFD7D5B0EC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ef0530ef18563772d3f741322062bf074cdc527e","datavalue":{"value":"Resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q4720797$4E73EE92-1BDB-4BC3-9FAE-436ABB4A7447","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"485447b25ea9ae3ba0e28b66b16f57c15b7c1fe1","datavalue":{"value":"types","type":"string"},"datatype":"string"},"type":"statement","id":"Q4720797$4EF7C6A3-0DE4-4029-9A7D-8FB6873E9AF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ecc2b9395f64ed6c1bc29d77571e5f996e7ffa1","datavalue":{"value":"higher- order unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q4720797$84CC4419-5016-4257-AD1B-F15A5790B39A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0cf667adfb3a7c2a0d960a5ec7dc6b4fdf525b48","datavalue":{"value":"Huet's search procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q4720797$1BA2998D-DC3A-4FC7-9485-38C1A9DA9C1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a61ba7de176f0a1a03dda8047dcca30f3428e59e","datavalue":{"value":"Martin-L\u00f6f constructive type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q4720797$A81B4023-D3AB-4C6D-BE3A-4514E93AA19C","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"c1c822e980808d04c28bee4c8ec18003cc39b2cf","datavalue":{"value":"Q55894613","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4720797$40AF1220-D948-48A3-83A6-8955479A4735","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4720797$BBA14E2C-9B7A-491D-9ED4-6490A60152D9","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":"Q4720797$CCB1721E-D376-41FA-B902-5D3F4C63F5D9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0da5ac60f79333aeef4cd9d2f815bccffb9243ed","datavalue":{"value":"https://doi.org/10.1016/0743-1066(86)90015-4","type":"string"},"datatype":"url"},"type":"statement","id":"Q4720797$9B0D6DF4-69E7-4328-9F6D-E071011425BD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"eb5edea4a3c5e10d17d04cd46bda29ce12e3ff5b","datavalue":{"value":"W2070577487","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4720797$66BFC3C4-278A-4E12-803F-88AFD1DD7FF9","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"9c63be36946c038de38adb7fede2b66984ba7a44","datavalue":{"value":"journals/jlp/Paulson86","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4720797$1EE560AD-BFBB-4207-B1DB-E31BDDAFAFB9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"afecd6c472083496ad86c6e9c17aaac9b0070f52","datavalue":{"value":{"entity-type":"item","numeric-id":4438235,"id":"Q4438235"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"07813f18372a571b0b63b579d52d29f1b04d184a","datavalue":{"value":{"amount":"+0.9493307","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":"Q4720797$901AA0E4-F1C7-4D3F-989A-0E5EECEEA685","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb7ba66d2c3227381ee1f820afe6e7f093220b1e","datavalue":{"value":{"entity-type":"item","numeric-id":5224775,"id":"Q5224775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"92151fb80d81d2bd94c53127c25d8a10d56c15ed","datavalue":{"value":{"amount":"+0.9162734","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":"Q4720797$585B5F85-C987-442C-A6E1-D0CE4463C2EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"44c2f64a6b4a61cc51aab7c09e2f2edd5d67249a","datavalue":{"value":{"entity-type":"item","numeric-id":3691668,"id":"Q3691668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c385280efb61cfce47b1cb825d7997aba2f88528","datavalue":{"value":{"amount":"+0.90766627","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":"Q4720797$DD05D744-A0D4-4041-8473-49D94B5278CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"57ad7e4eca72a694345060d15fef735922b1f6d2","datavalue":{"value":{"entity-type":"item","numeric-id":4982108,"id":"Q4982108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d2ddc8ea6925022722952f921335716abadc3fff","datavalue":{"value":{"amount":"+0.90268993","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":"Q4720797$2B8F9B57-7D0C-4C8D-B717-E7C30EB14620","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"849ca33231c4feda7d3112ba6036c47e5d9eba02","datavalue":{"value":{"entity-type":"item","numeric-id":1813231,"id":"Q1813231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7c7b9821365e40ff6cee499ffac354e3e721bde1","datavalue":{"value":{"amount":"+0.9011351","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":"Q4720797$6CFBE218-3185-4B99-837A-3CA845761A4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c0243f4d23771544088dce9ece1c4730ffdede91","datavalue":{"value":{"entity-type":"item","numeric-id":1577342,"id":"Q1577342"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8ba72c71fe483a88644b7e813c7bd7d08adfbe37","datavalue":{"value":{"amount":"+0.8991755","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":"Q4720797$7491D5CC-6D68-4333-AF49-B176E465F5AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"21aa2fc351b7bd12bae8a271be1dcd96021a9397","datavalue":{"value":{"entity-type":"item","numeric-id":1577346,"id":"Q1577346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"85ba7fdcbb5bbcaa55ae10ff7152ff963f0f67fa","datavalue":{"value":{"amount":"+0.8982048","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":"Q4720797$15A00FC4-DC74-4CD9-84F2-70AE54F5A333","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00208d8e95432131ada27b43b8097d607ab26759","datavalue":{"value":{"entity-type":"item","numeric-id":2746598,"id":"Q2746598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9a679c2f9f084e3e01cc110a4aba5625cc1b11bb","datavalue":{"value":{"amount":"+0.89755636","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":"Q4720797$C7531B29-11AF-490B-BA74-2AA1F60068A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce256adef124d09eb756ed038608701398011fab","datavalue":{"value":{"entity-type":"item","numeric-id":4294473,"id":"Q4294473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"238051639ed458f349b23f25ee47634d0075fe19","datavalue":{"value":{"amount":"+0.8960538","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":"Q4720797$86F9429F-6C3E-47EC-A55D-0073D1505C25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69b994e8d0c268ef50f80de07a97940db98d609a","datavalue":{"value":{"entity-type":"item","numeric-id":4820470,"id":"Q4820470"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d88c3df9c5ee40a2560a35ebc2ab9138da8a2cad","datavalue":{"value":{"amount":"+0.89593315","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":"Q4720797$BD7D7867-8B95-4E31-9023-0AADC52D4C57","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4720797","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4720797"}}}}}