{"entities":{"Q1107510":{"pageid":1118259,"ns":120,"title":"Item:Q1107510","lastrevid":69659259,"modified":"2026-04-13T08:31:30Z","type":"item","id":"Q1107510","labels":{"en":{"language":"en","value":"The addition of bounded quantification and partial functions to a computational logic and its theorem prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4064955"}},"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":"Q1107510$30F3D91F-680C-4737-B43C-6C88F4A3FD3F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cb8f97a90ca0710368f4f2cc41600e21ff9ea6e0","datavalue":{"value":{"text":"The addition of bounded quantification and partial functions to a computational logic and its theorem prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1107510$BD4D2649-2093-4947-B382-07DBCB0361EA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7906cddb7309f22c29d77ae15f7291c139a8fc49","datavalue":{"value":"0653.03007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1107510$ADCC5CDC-D8A3-48B6-83FD-60FA1955DE19","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"45626a0cdbd3045fcd6a4aaa18791327ee3f9626","datavalue":{"value":"10.1007/BF00244392","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1107510$5B3C9AFF-3CF1-4032-B87A-C6FF2021008F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"43c80439908def1f47a2850b299ced02bb922e89","datavalue":{"value":{"entity-type":"item","numeric-id":861688,"id":"Q861688"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1107510$15428F07-2BDF-4A4C-89EC-7B54A10A5126","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b0d384413a2d1b8185eb46b74e5b2c74244e0aac","datavalue":{"value":{"entity-type":"item","numeric-id":928667,"id":"Q928667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1107510$D3A791B3-D1CC-4322-A0FF-4BD0FEE52108","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":"Q1107510$A3EC3BAE-393E-4963-BB22-F5C47E3157ED","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"31a1937240ca4a323604b4728c31d242b5596d7c","datavalue":{"value":{"time":"+1988-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":"Q1107510$AF958259-93FB-4BEA-A790-AA4D50013EC8","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"2f09ee5bc8fe6ac9586308fdfa165badf55ff612","datavalue":{"value":"The paper describes an extension of a computational logic, developed earlier by the authors, by bounded quantifiers and partial functions. Bounded quantifiers are variable-binding constructs with the bound variable ranging over some finite sequence. The formalization employed also includes partial recursive functions.    The computational logic which the work is based on is a quantifier-free first-order logic resembling pure Lisp. An extensive automated theorem prover has been written by the authors and shown to be able to check proofs of rather complicated theorems. The formalization of the quantifiers extends the existing logic and the theorem prover with additional constructs providing mechanisms for controlling the elementary operators of the underlying theories. Basic properties of the formalism are studied, and the use of the extended logic and its theorem prover are illustrated on construction of several proofs, including a proof of the Binomial Theorem.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1107510$4353D829-7C2A-4DE0-A41D-C32B4970E599","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1107510$FDB0A618-EC9A-4AF7-A478-EAADA85DE66F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1107510$D3B32F64-74FA-43FB-BD21-7B30EBF09D68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1107510$2B99EF8A-8842-4116-ADEC-04EAED538034","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1107510$5875D642-82DD-4225-97D0-C4CD2A1CF6C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d8724ac1f861fd4485a474d1844744a1ace24834","datavalue":{"value":"03-04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1107510$A64DF33D-2390-409D-AE2A-AA3D71D1EE11","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1f949502f2b5675fdee3ce3a8769a26cbff4df9f","datavalue":{"value":"4064955","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1107510$29327394-485A-4068-BB03-58785A943A02","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0f796ed2b460346bbba92264dac0da22a5120d5d","datavalue":{"value":"recursion","type":"string"},"datatype":"string"},"type":"statement","id":"Q1107510$A3E2090A-F260-4DAD-99F8-C870929D3F0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"40f75c475f47e64366621547454dd16d54565743","datavalue":{"value":"interpreter","type":"string"},"datatype":"string"},"type":"statement","id":"Q1107510$5CE42C86-5F41-44D1-9E92-13066F2D14EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cf24d89f4f0821f90ed933db7d403c989feed0ad","datavalue":{"value":"evaluation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1107510$40619E70-C239-49AE-A820-194E484D15F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d7bfc11de8cab95fd6af201970bd9d16d39bbd0","datavalue":{"value":"semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1107510$3DE55537-1F30-455A-A97B-410CB4FBA324","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"27c2e420b7a7dc3b2d33a778c4052dde05e3b536","datavalue":{"value":"continuity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1107510$EAE7419D-163A-4692-9B20-EFE047610F13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dbec5c2b93e66e86aa0d97f1c5c6e6aacaff7fc6","datavalue":{"value":"computational logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1107510$0E906010-C834-4D26-ABC6-1F946698D5EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c29147387eed55a0f3f8fd87c7777123189944d5","datavalue":{"value":"bounded quantifiers","type":"string"},"datatype":"string"},"type":"statement","id":"Q1107510$6AF75062-7BC9-456A-B7AE-FFF597757C8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d31be1229374545ff94fd95ad2a5ce9870f120db","datavalue":{"value":"partial functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1107510$A93DF279-A9D9-483D-A6CA-1FFEC67863B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c921490c1125c361e971a89c1373bf2f0970a7c9","datavalue":{"value":"quantifier-free first- order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1107510$A3D3DCBC-4E86-4B46-8628-F96AE0F14711","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"06fb2c2146a125b3ece962edb8f131612526f24f","datavalue":{"value":"pure Lisp","type":"string"},"datatype":"string"},"type":"statement","id":"Q1107510$D2481A36-0C62-4AD2-9D1F-B1B1515B3D87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5fbe3c7285c82b7e85a0384689c42c38ba7418e4","datavalue":{"value":"automated theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q1107510$48EE1956-D388-4AA3-BCDA-B231C2C029A7","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"828dfc38786d2049fd79af4c315ff0a16e6bc429","datavalue":{"value":{"entity-type":"item","numeric-id":1188836,"id":"Q1188836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1107510$93C0CEA5-BAB7-47F1-AA61-68ADD91623BC","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1107510$8B2CDCD4-7504-4052-9B22-8AE1F3A3AA05","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":"Q1107510$F90065DE-EE65-43C3-B24F-838222C84F53","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cbcd10007bd797ac95edbb89da8259071d2eb01f","datavalue":{"value":"https://doi.org/10.1007/bf00244392","type":"string"},"datatype":"url"},"type":"statement","id":"Q1107510$E6BB923E-11F2-4C67-9FE6-845B98C956CE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"39e75068ea4ae594ee2573859acec0cd8d8b913c","datavalue":{"value":"W4248504484","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1107510$732AA914-E628-4EE8-A221-04EE5ADF88AF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3cda481b541398e1a99f4b5d3ef12a328b1ce13e","datavalue":{"value":{"entity-type":"item","numeric-id":6488518,"id":"Q6488518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"08aa5b8b930aa964d7a2acf98cd851bc8d9e78c5","datavalue":{"value":{"amount":"+0.7587381601333618","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":"Q1107510$94F5C24E-DC9F-4164-9739-AEB64B018E81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab43f2ae37318e013baee643a395be18b9c2596f","datavalue":{"value":{"entity-type":"item","numeric-id":4040283,"id":"Q4040283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8fa197a1c0f4c7be59281d2bf6907e049133335","datavalue":{"value":{"amount":"+0.754715621471405","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":"Q1107510$BDB3C173-8AFE-4AFD-9829-CB402C765BB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"77dd6e8b3716ac8815a409e6de120987392d573d","datavalue":{"value":{"entity-type":"item","numeric-id":688572,"id":"Q688572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4658b459537f92f20f9749961b80f4fab138ff37","datavalue":{"value":{"amount":"+0.7367417216300964","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":"Q1107510$B6E98C5A-F885-45BF-8531-C883F353B7CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"880184504bd47d4aab173f44873bb04dbe6f5cfc","datavalue":{"value":{"entity-type":"item","numeric-id":1309243,"id":"Q1309243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c52c991026a422ef3c714072aa3169e3593ef399","datavalue":{"value":{"amount":"+0.7350136041641235","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":"Q1107510$F722AD49-8D6B-4BA4-895F-97CDC35D9226","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad894f0e4fcd4cc03c848bf583b58ab56e3b8f5c","datavalue":{"value":{"entity-type":"item","numeric-id":2753786,"id":"Q2753786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9731902544a24bd3d3c032dbfda9f9c7462f9a71","datavalue":{"value":{"amount":"+0.7293550968170166","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":"Q1107510$977E0245-9C78-4C01-9A20-8FCB218982BC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The addition of bounded quantification and partial functions to a computational logic and its theorem prover","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_addition_of_bounded_quantification_and_partial_functions_to_a_computational_logic_and_its_theorem_prover"}}}}}