{"entities":{"Q1066880":{"pageid":1077632,"ns":120,"title":"Item:Q1066880","lastrevid":66074331,"modified":"2026-04-12T07:21:54Z","type":"item","id":"Q1066880","labels":{"en":{"language":"en","value":"A decidable fragment of predicate calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3926875"}},"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":"Q1066880$D0563DCC-2647-425C-B572-9FA95E207EE4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1ac1f96ce4f7d1ddd2d189d78c673b302314662a","datavalue":{"value":{"text":"A decidable fragment of predicate calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1066880$20C1E508-5714-480D-8240-5B7FC2967311","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4bcacad88fc33bb4b0c380833042ba188f9fbce3","datavalue":{"value":"0579.03007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1066880$7FFECD38-6EA3-42BD-B4A9-6B6C6B8DD964","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"583fee7e4152c9e119ab586e18bea81e50278755","datavalue":{"value":"10.1016/0304-3975(84)90047-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1066880$F9FFFB0C-2975-4849-8F7D-DBE9A2094A71","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2a5ae867760d8ac8c576f6f7d4130b2635044bdf","datavalue":{"value":{"entity-type":"item","numeric-id":755599,"id":"Q755599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1066880$BDAC7E16-EE66-4526-9BD0-4441021AD819","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7e2f1fd6f2929b6653b631272c22fa4df2c93bf4","datavalue":{"value":{"entity-type":"item","numeric-id":1140435,"id":"Q1140435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1066880$BE511F85-F8E2-439E-A1B5-0907985ED9B0","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1066880$2EF79268-EAC4-406A-BC52-0B8494261E08","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ee0f220147ae8bc749a64db56839865dbc4f127","datavalue":{"value":{"time":"+1984-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":"Q1066880$584AD6F9-B7C5-4716-B230-1C6BCF2BB79C","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"2fedd839c0f32218adc1778559df6e66c5b76063","datavalue":{"value":"The authors describe a fragment of the pure predicate calculus which they call direct predicate calculus. It coincides with those formulas that can be proved in the Gentzen sequent calculus without the contraction rule. The direct predicate calculus is shown to be decidable. The procedure first brings a formula into a normal form (in linear time) then applied a characterization of valid sequents in this form.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1066880$722617EC-40AB-49E0-BE5C-8F0F29EEE62D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1066880$4344A708-512F-4541-A151-875DB0190769","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1066880$2674AF7E-67F2-45D7-A49B-B11CF6C09437","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1066880$B2998AC3-F9AA-415D-ADAB-D1368602C8A7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c34b4f46ef8a38f546a094de94c0fcd595771498","datavalue":{"value":"3926875","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1066880$19CAE0A4-ADFD-47FB-B290-6CA2D0AA753F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"30d4ed2f35f6e73acfa0b633a974ed20c81014ef","datavalue":{"value":"direct predicate calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1066880$1CF60503-848B-453B-BC26-98ADAEEF76CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5e29b93e0b70a3f3e4ffd77cc53b1ae58481c2d5","datavalue":{"value":"Gentzen sequent calculus without the contraction rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q1066880$4984FB21-0E6B-46EE-98F9-D6793CD12A7B","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"49ac28ac151a8a9103bbae52e8a00e91b3069fd7","datavalue":{"value":{"entity-type":"item","numeric-id":590477,"id":"Q590477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1066880$4179640B-856B-4AB0-B84C-74E7716E69DA","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":"Q1066880$05E43AEC-8735-40ED-BF46-18AA2C068099","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b57a7d4be542fbed1aaa093d6eae5500ffe2f68d","datavalue":{"value":"https://doi.org/10.1016/0304-3975(84)90047-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q1066880$69F47244-19AE-4745-AA9A-852E053922D4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1972b84ca88775de272c3d244a48e7c7a7dac79f","datavalue":{"value":"W2057599103","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1066880$DA457EF4-255D-42CC-A391-662797652B83","rank":"normal"}],"P223":[{"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":"Q1066880$5AD88A00-89CA-46D6-9EA8-ED302E56E141","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9d6412374cd99d26f25760aacca4ecd0fb813a7","datavalue":{"value":{"entity-type":"item","numeric-id":5339307,"id":"Q5339307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1066880$2EE16C2E-7478-42E2-8277-028E9DFF2856","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb103918e031217ff37d103578191225b1a433c7","datavalue":{"value":{"entity-type":"item","numeric-id":5843956,"id":"Q5843956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1066880$D8FEE2F4-4074-4C30-AAF1-D40DAD1107B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"daa75d76e1cdc609f7ac46974607202a4c628e1e","datavalue":{"value":{"entity-type":"item","numeric-id":3275832,"id":"Q3275832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1066880$C2F76DF6-52AF-4F60-AC57-BFC71E9B7B4D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e73c792c37d84ab03b8dbe2def263e976cf7aaf3","datavalue":{"value":{"entity-type":"item","numeric-id":1186430,"id":"Q1186430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"15cec16748b8104e66a361b190e8129d66640448","datavalue":{"value":{"amount":"+0.8622353672981262","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":"Q1066880$E41E95F5-9113-41C5-BB6B-CBD7C9514F00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a1a12c1e0a5a77e2f0e3ee42f30fdeb4e0ae403","datavalue":{"value":{"entity-type":"item","numeric-id":4948542,"id":"Q4948542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"01f6d72c896fea0d5353001488664d48b5be51f0","datavalue":{"value":{"amount":"+0.8562766909599304","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":"Q1066880$76D272D8-E620-44C3-A62F-1C9EF12A47A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69bcbe76f08c7ee674920a9484d3e4a20a3b32a9","datavalue":{"value":{"entity-type":"item","numeric-id":5460923,"id":"Q5460923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2f692700db1e8c812102a2071f230559c4e40d4e","datavalue":{"value":{"amount":"+0.7962484359741211","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":"Q1066880$ECDF12FB-E068-4CB5-AD83-E6AFC908624D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"20f675bfafec1d8faa1d6cd68fc939a3471da341","datavalue":{"value":{"entity-type":"item","numeric-id":3520225,"id":"Q3520225"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6e2bab4d087354441fb22f8958d3c8e23af74262","datavalue":{"value":{"amount":"+0.7748842835426331","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":"Q1066880$0C27D7CF-AE9B-4F82-BD9A-832B0661BA36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5872fc21b5f419b387964f6b17c691f7e732f609","datavalue":{"value":{"entity-type":"item","numeric-id":2503325,"id":"Q2503325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"850894d2d116deee553b6c659a8af050a5353e3a","datavalue":{"value":{"amount":"+0.7533196806907654","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":"Q1066880$8F230A02-CD85-411A-AF08-354E84140D55","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A decidable fragment of predicate calculus","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_decidable_fragment_of_predicate_calculus"}}}}}