{"entities":{"Q1049689":{"pageid":1051537,"ns":120,"title":"Item:Q1049689","lastrevid":69509010,"modified":"2026-04-13T07:28:49Z","type":"item","id":"Q1049689","labels":{"en":{"language":"en","value":"Proof-finding algorithms for classical and subclassical propositional logics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5657219"}},"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":"Q1049689$C62571D7-74E7-4142-8D77-E6DAF62DB887","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7be52153e9919933faeea77c76cb7c02e82507e0","datavalue":{"value":{"text":"Proof-finding algorithms for classical and subclassical propositional logics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1049689$794A7643-A95B-4DB8-A0E8-700DFA398649","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"aee683b4829cf2ad573f082d557f44bbbe070b46","datavalue":{"value":"1202.03024","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1049689$AA406EBB-B05B-4E2A-B65D-853AB320472C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e1e2879ea3f87fd57a0cf39fd3babf00ad2ce157","datavalue":{"value":"10.1215/00294527-2009-011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1049689$530DE25A-201D-4883-86CB-63E8C6CF9EC5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"876b0df6650f37e58f68ae198ab9500c4119ce8e","datavalue":{"value":{"entity-type":"item","numeric-id":1049688,"id":"Q1049688"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1049689$569A6BAF-44DC-426F-95EB-A605C595ADC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5d7a7742b54ec2d03c259f24892f02db2125d6a2","datavalue":{"value":{"entity-type":"item","numeric-id":591019,"id":"Q591019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1049689$13DA12A4-7CA5-49B2-84C3-B06A31AB7B60","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6325d9f59cde8ebbdb24a9f950cab3fcef3decf6","datavalue":{"value":{"entity-type":"item","numeric-id":190248,"id":"Q190248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1049689$BFB439CC-FE03-4F56-8C0A-C0712B96FB5D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"881d7755ed56ad45091e513ac6c64caeecaa15ad","datavalue":{"value":{"time":"+2010-01-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1049689$D39AFB8A-3551-4CBB-BA46-88E3A3FA97EC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a897480767112217a19e3ea4b79defb5e0b5f29a","datavalue":{"value":"The Curry-Howard isomorphism allows proofs and theorems of intuitionistic implicational logic to be represented as combinators or lambda-terms and their types. The results in this paper rely on work by Trigg, Hindley and Bunder who showed that, for a large class of logics weaker than intuitionistic implication logic, proofs can be represented by restricted classes of lambda terms or combinators. This work was used by Bunder to develop proof-finding algorithms, most of which have a bound on the number of steps required to produce a \\(\\lambda\\)-term proof, or a guarantee that there is no proof, based on the structure of the formula being examined.  In this paper, the authors extend these algorithms to the following logics with additional connectives:  {\\parindent5mm \\begin{itemize}\\item[1)] Logics with minimal negation, i.e.\\ extensions obtained by adding a constant type \\(f\\), which is used to define minimal negation. \\newline A general class of Q-logics (Q-type theory), called MQ-logics -- which include connectives defined using \\(f\\), and, in particular, also minimal negation -- is introduced. A proof-finding algorithm for MQ-logics is given. \\newline Intuitionistic versions of the relevance logics \\(R_{\\rightarrow}\\) and \\(T_{\\rightarrow}\\) are among the logics to which this algorithm applies.  \\item[2)] Logics with implication and intuitionistic negation, i.e.\\ extensions of type theory to include the axiom \\(\\vdash F: f \\rightarrow \\alpha\\). (Here, \\(F\\) is treated as a combinator with \\(f \\rightarrow \\alpha\\) as its type.)  \\item[3)] Implicational logics with Peirce's Law and minimal negation, i.e.\\ extensions with a ``combinator'' \\(P\\) with Peirce's Law as its type.  \\item[4)] Full classical propositional logic (based on the types of \\(F\\) and \\(P\\) and of the standard combinators \\(K\\) and \\(S\\)).  \\end{itemize}}","type":"string"},"datatype":"string"},"type":"statement","id":"Q1049689$16AAD0D1-478C-4BEF-8888-F2BD47AF7C17","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"895d5fc798d777f77a43df1e1b11857e28584cdd","datavalue":{"value":{"entity-type":"item","numeric-id":592080,"id":"Q592080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1049689$8FD89071-E8D0-4048-A91B-2AA25BD1AC4F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1049689$2BD017C4-CBD1-48B4-A7C9-3D1270778F23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1049689$1AEAEB07-4454-4F26-A110-7BB560F2AFC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1049689$5CDFC4A3-E127-4975-B24D-0FFCDC2E9C96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b363e494c684597e57f0cc15c7c0d8f9f3bcf9fc","datavalue":{"value":"03B47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1049689$F66397DA-30E2-42A8-98A3-9872A1ADF562","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5869853aba4218721191af141b42534e89494712","datavalue":{"value":"5657219","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1049689$938EE913-C8A5-4383-9463-26915AC2FDDF","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":"Q1049689$7B70CA51-BCCA-4A3D-81BA-AB05268645A3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f5e40f9d35a7ee329d9a85eff4e6a9474c6ce9eb","datavalue":{"value":"https://doi.org/10.1215/00294527-2009-011","type":"string"},"datatype":"url"},"type":"statement","id":"Q1049689$1DB8E42D-2708-418B-BB2C-335837A7133C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"12bb14978b41f6c8e7522b5fb4db39631ab7f579","datavalue":{"value":"W1998289751","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1049689$C460FF91-38C9-4E9D-9379-7723853E3D3D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"523ceda9c46f837435b012e3131d159e916a802b","datavalue":{"value":{"entity-type":"item","numeric-id":1575928,"id":"Q1575928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"28c17d4b2d6d05716637a2e0eb87e53b133cfc40","datavalue":{"value":{"amount":"+0.851446270942688","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":"Q1049689$AEF85432-9E1A-4872-A34C-533149A4463E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8a40b525022ec1dccaba201ae6fd7476bf823c4c","datavalue":{"value":{"entity-type":"item","numeric-id":4856946,"id":"Q4856946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1e2a8e29a5fb75a512c5521a3ecaecab362e18bb","datavalue":{"value":{"amount":"+0.769162654876709","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":"Q1049689$13B562C8-F215-4AD3-9A01-1FFE94B828CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2e653c6a3446968fd019febeccb6f5e0a749547d","datavalue":{"value":{"entity-type":"item","numeric-id":2757810,"id":"Q2757810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b3728bfd16fbde4c5bf956c20f07d7f1b515cba1","datavalue":{"value":{"amount":"+0.7656155824661255","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":"Q1049689$3B259DB6-B258-45B6-B404-5A50BE54F948","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"61bd3300c7dc67e2bc56e6bd1256442b32e9f142","datavalue":{"value":{"entity-type":"item","numeric-id":4645244,"id":"Q4645244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88003a32157e3fc976928ee1a77f15e8c8d314e2","datavalue":{"value":{"amount":"+0.7638853192329407","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":"Q1049689$A9FBD456-5B77-4C42-9421-39C8C755010B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c715127c8e152ee2bfee86db84fa47a5e01e6591","datavalue":{"value":{"entity-type":"item","numeric-id":1575923,"id":"Q1575923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"29c682338cefddf5bd62aa4e582e40596812f439","datavalue":{"value":{"amount":"+0.760492742061615","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":"Q1049689$17169732-2868-4008-B3FF-CEFECF3B4AB5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof-finding algorithms for classical and subclassical propositional logics","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proof-finding_algorithms_for_classical_and_subclassical_propositional_logics"}}}}}