{"entities":{"Q1187858":{"pageid":1198607,"ns":120,"title":"Item:Q1187858","lastrevid":66447258,"modified":"2026-04-12T10:08:46Z","type":"item","id":"Q1187858","labels":{"en":{"language":"en","value":"Automated deduction in von Neumann-Bernays-G\u00f6del set theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 39774"}},"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":"Q1187858$2A58F0D1-4909-4407-9FB7-1351B6EC3383","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"37c539955794809f2f14fd6a7e4c40aa80ceb699","datavalue":{"value":{"text":"Automated deduction in von Neumann-Bernays-G\u00f6del set theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1187858$DDEC6170-6FA6-415C-B855-94E983C68C0D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2c9224c235d2f3d6764e2322cfc929afc0ec2ca3","datavalue":{"value":"0768.03005","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1187858$A6B6F492-A5A1-4AB8-8E98-F3279DDA7B24","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2d616334ee27272dfd5edd79aff6bd7b71dad7c4","datavalue":{"value":"10.1007/BF00263451","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1187858$9DCCE938-F4A8-4B78-9289-B39902B44BC7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5921f6a95e23e242ab9096b29af3ddddabf98db7","datavalue":{"value":{"entity-type":"item","numeric-id":1110494,"id":"Q1110494"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1187858$380B09D3-4438-4C94-965E-001275DA9122","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":"Q1187858$7E40BA64-F4DE-4C04-AD3C-4CACAC8D0235","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c773167c26a162b23b65174f7b507d41ddb43a31","datavalue":{"value":{"time":"+1992-07-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1187858$64CC58D9-BBCE-4484-BEAA-4EE2561FC38D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"7a37f0871ee2d47c245223e6880a8bffa6beea40","datavalue":{"value":"This article is a journal version of the author's thesis, which has been published as a book [Automated development of fundamental mathematical theories, Automated Reasoning Series, Kluwer (1993)].   The objective of the work was to find an axiomatization of set theory suitable to treat with first-order predicate logic theorem provers. To this end a clausal version of the von Neumann-Bernays-G\u00f6del axiomatization of set theory was developed and over 400 theorems were proved using the resolution-based automated theorem prover Otter. A number of heuristics and tricks are presented for guiding a theorem prover and proving quite complex theorems, including Cantor's theorem, at least semiautomatically.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1187858$23A908A3-E9E2-4C43-965A-262E608A7258","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1187858$665CE8A8-FC31-4E73-8F58-6F733889B710","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2b0919c48a255b26fcf065230a9a621cd8c579a3","datavalue":{"value":"03E70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1187858$63AA64F1-D720-4AAA-8453-AAAF2872DB27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1187858$CBEA49DA-C65B-42AF-8FD9-A89C06DFF61B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"de0ed20f8b898ce636e9d77c5dfcfb2e35cc02d2","datavalue":{"value":"39774","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1187858$1B669A62-91A1-4B8B-8111-ADA6E30A1578","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5e8d9a59cc3cb8cf1b8734d162b0e085235b9d71","datavalue":{"value":"clausal version of Neumann-Bernays-G\u00f6del axiomatization of set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1187858$608903EE-40CB-467B-8BCC-CFD1EF6678FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7432134684d87b98a3fe34c30cff0e5ef039d2c5","datavalue":{"value":"resolution-based automated theorem prover Otter","type":"string"},"datatype":"string"},"type":"statement","id":"Q1187858$E3E6BD4E-1397-4B7F-B1D8-A61CD0E7119D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a0ffcc3545bd7b0f94969c35c641231860a38c51","datavalue":{"value":"heuristics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1187858$84136D2B-E1CA-4CA0-87DA-B63E1CB381F0","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"29d85a164d09045374c4187cab59d334a70ca718","datavalue":{"value":{"entity-type":"item","numeric-id":1097715,"id":"Q1097715"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1187858$8EC91F27-65F0-4373-9133-427F09B9238E","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":"Q1187858$DA2AEF9B-E34B-424C-94DC-857BD366AD11","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"938518b32406a40fda054f044cd2e03aca72cdb5","datavalue":{"value":"https://doi.org/10.1007/bf00263451","type":"string"},"datatype":"url"},"type":"statement","id":"Q1187858$D27F4840-6573-46AE-8470-E00FD5D65CD5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"cb2110eaaa6fcc80a2a22e4fc3a48caf36857d80","datavalue":{"value":"W2041161966","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1187858$6E261730-0A23-4240-8200-F992CE11149B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"50074d6557af33f5fd1960d631eb058e98c4ebcf","datavalue":{"value":{"entity-type":"item","numeric-id":1097252,"id":"Q1097252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"779a56042d186e81ad85cdf769893658dfaaf495","datavalue":{"value":{"amount":"+0.8189516663551331","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":"Q1187858$F5F603EF-92B1-47E3-8411-580011030B89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18fef7ff67e321f5da285458ae23b57701a5f98b","datavalue":{"value":{"entity-type":"item","numeric-id":4032144,"id":"Q4032144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b345a0b06c1bf3e4ed1821e490b79e9f41db4193","datavalue":{"value":{"amount":"+0.8106642961502075","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":"Q1187858$4C899764-FF9D-406E-BFCA-75107B984EB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d8213c84e722b981af05319a6ca2089cbbe9522","datavalue":{"value":{"entity-type":"item","numeric-id":2457343,"id":"Q2457343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"edb9f408eacee7ed0a4899b6673356be7df41796","datavalue":{"value":{"amount":"+0.7881042957305908","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":"Q1187858$2A9516A9-B987-497D-AFFD-8EDA130EF9F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"039c873276c470bee9e8337c738ab0cb44cc25ee","datavalue":{"value":{"entity-type":"item","numeric-id":3812202,"id":"Q3812202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a376470675bab2d5ed955982f86cd8e438b5898c","datavalue":{"value":{"amount":"+0.7652505040168762","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":"Q1187858$53B20D51-FAFA-4032-97FB-932F9AB644DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7d53e3269671c3b829332645636422f0534f2837","datavalue":{"value":{"entity-type":"item","numeric-id":4707766,"id":"Q4707766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b21f52a90f30c09195014a009f6041848d87a80","datavalue":{"value":{"amount":"+0.7505637407302856","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":"Q1187858$8DFBB414-E2FB-4FCF-A241-1985B0FA83E1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automated deduction in von Neumann-Bernays-G\u00f6del set theory","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Automated_deduction_in_von_Neumann-Bernays-G%C3%B6del_set_theory"}}}}}