{"entities":{"Q2761749":{"pageid":2772488,"ns":120,"title":"Item:Q2761749","lastrevid":83145377,"modified":"2026-05-07T06:17:53Z","type":"item","id":"Q2761749","labels":{"en":{"language":"en","value":"Embedding first-order logic in a pure type system with parameters"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1686293"}},"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":"Q2761749$AB907678-3E3C-4261-BC32-7B1A15470740","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a61d8506481fabfe5f58e6605c0ce0a37cc7205e","datavalue":{"value":"1006.03014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2761749$F3B44CC9-A741-4BF4-B384-7725BB014DBE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a5833a50b9b6136fe4d80f55956accec8d2089eb","datavalue":{"value":{"entity-type":"item","numeric-id":195252,"id":"Q195252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2761749$1CF894B0-F0AA-4A02-83E2-A9709008DB9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3717bd40e47595e2a7f112a055a28e3a189d2344","datavalue":{"value":{"entity-type":"item","numeric-id":2711193,"id":"Q2711193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2761749$23CE8671-5F95-4433-93CF-E5B0155A758A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"dd23d86f8a62e2a287b0d3c845d667edeacbe3e6","datavalue":{"value":{"time":"+2002-01-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2761749$6B2D0EB9-5604-4371-876B-502A0CF5F0F3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2761749$F1552751-0958-4290-8DFF-F76AF6E96941","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2761749$150E286B-46CC-4ABB-B882-494384A16B78","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"498888a87cd9e42bf5226e86c14b12e0966c124a","datavalue":{"value":"1686293","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2761749$C30967D0-0919-4F95-BBEE-25E9EAF3FAE4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6dfe1644ac541db27a48b44818ebdf600ca6237a","datavalue":{"value":"\\(\\beta\\)-normal form","type":"string"},"datatype":"string"},"type":"statement","id":"Q2761749$1E8F1D8C-9837-4CA2-B96B-7D7A2E0BFE55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2761749$8F1CD585-8880-4631-83E9-292220266E97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f182e86329a34e1b4cc75d54bcc34cbb69c421c6","datavalue":{"value":"typed \\(\\lambda\\)-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q2761749$315E2252-639E-44BE-A55E-F602C50A9323","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f4cee31b109bfd0275ef9410b844f3bfc242cf31","datavalue":{"value":"first-order predicate logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2761749$FB1BAECC-D7D2-48DA-8D10-41CFF6CC47A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f383f0654f5901fb84059190f1909ba97246c04f","datavalue":{"value":"pure type system","type":"string"},"datatype":"string"},"type":"statement","id":"Q2761749$AC8FF2CE-9811-43FC-BC4E-7C01B262EA44","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":"Q2761749$63027083-8EEB-48F1-A760-CB7A21CC3B3F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ba64d47475b7e2d61b45437f7ab58a132226bd03","datavalue":{"value":"https://doi.org/10.1093/logcom/11.4.545","type":"string"},"datatype":"url"},"type":"statement","id":"Q2761749$F1F4FC57-2166-4805-AC35-38DAC1CC75A5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"11dde310decda91a1394f915700b000d798f0d88","datavalue":{"value":"W2104816023","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2761749$7B47EDE6-B9C1-4F08-B158-9922A4141E42","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b0cff1d79bc00be2508c9d30d29a35ef7a245055","datavalue":{"value":"10.1093/LOGCOM/11.4.545","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2761749$F2B0407C-E676-4771-BB31-6C5470F64ACE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"80bf495de81d80862fe8032af8051cf86ce73d4c","datavalue":{"value":{"text":"Embedding first-order logic in a pure type system with parameters","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2761749$A51784F4-27AF-424A-A416-FCC998623498","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4e284497c1d95ed03031b32369f55bf404c9e002","datavalue":{"value":{"entity-type":"item","numeric-id":6768690,"id":"Q6768690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2761749$B2110CD5-9936-4564-AFE5-44AE13E6EE74","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"9b2e5c34f31574911f5cef8a76f8c772b1726bbc","datavalue":{"value":"A standard way to code first-order predicate logic in a propositions-as-types style uses a type system that is a variant of the pure type system \\(\\lambda P\\). Types in this system are not necessarily in \\(\\beta\\)-normal form. Therefore, checking whether two types are \\(\\beta\\)-equal is decidable, albeit sometimes costly in terms of time and/or memory. In this paper we present an alternative to Berardi's system, based on pure type systems with parameters. We show that all types in our system are in \\(\\beta\\)-normal form, which is an advantage for implementations. Moreover, the syntactical structure of the system with parameters is similar to the syntax of first-order predicate logic. This is not the case for the system without parameters.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2761749$556CC2CD-A6DB-4BE6-8C74-56A870E170D1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2c1b218eed2a7a863f8eea76b1b401f765205d23","datavalue":{"value":{"entity-type":"item","numeric-id":4223028,"id":"Q4223028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"93e1f054f31a86e4ff26ccddd85440ed7fbcf1e1","datavalue":{"value":{"amount":"+0.8027072548866272","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":"Q2761749$14588CA3-D246-491C-B5B4-0702BCA56BA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4c41dc7be02d86f7446c3b051219b56c92c6dbce","datavalue":{"value":{"entity-type":"item","numeric-id":5248986,"id":"Q5248986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"916717f66a00f7f908f7bd1b3ef8c19d5c0e655c","datavalue":{"value":{"amount":"+0.7511113882064819","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":"Q2761749$A502E380-FB13-44B4-ADF5-AD4FF2754031","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"751e935b2cd35d976df2f1709e3d83b3d0fa2611","datavalue":{"value":{"entity-type":"item","numeric-id":4704760,"id":"Q4704760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f04f70b1a85e5a5682d7787102a006abc265d2ab","datavalue":{"value":{"amount":"+0.7451487183570862","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":"Q2761749$2C068374-5C3E-4820-84CF-0DE064B4ADC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"192016c7411dd01638c7d001c7b6a59d7fb8d10b","datavalue":{"value":{"entity-type":"item","numeric-id":1260645,"id":"Q1260645"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f04f70b1a85e5a5682d7787102a006abc265d2ab","datavalue":{"value":{"amount":"+0.7451487183570862","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":"Q2761749$C7562BF1-9514-4852-A5A7-33CBDEB8F88A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"56b13e65f3dbf5f4223ceeefebb92f0260fb072f","datavalue":{"value":{"entity-type":"item","numeric-id":3044340,"id":"Q3044340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"06b1c2ee724c2dd6459a8238b14d1421a2e66b6a","datavalue":{"value":{"amount":"+0.7438690662384033","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":"Q2761749$09414A3E-4318-49CE-9E7B-4A25BDB6DAD5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Embedding first-order logic in a pure type system with parameters","badges":[]}}}}}