{"entities":{"Q651313":{"pageid":653162,"ns":120,"title":"Item:Q651313","lastrevid":63324174,"modified":"2026-04-11T12:06:13Z","type":"item","id":"Q651313","labels":{"en":{"language":"en","value":"A constructive investigation of satisfiability"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5987965"}},"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":"Q651313$12CE0FE1-95A8-486C-B8E0-7C27ACA41E5F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0e9d328908f104bbcd27bfedb509c278f03e13c4","datavalue":{"value":{"text":"A constructive investigation of satisfiability","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q651313$20012D35-6927-428E-BDC5-D837801C9B08","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"378faf845d3d44594bc6a7fa97936429f8b8889f","datavalue":{"value":"1246.03023","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q651313$074F818A-07E3-4467-BCA3-5F97C860073E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a3805f594ddac6fae8f2d2362aaebc83c0fa4374","datavalue":{"value":{"entity-type":"item","numeric-id":290641,"id":"Q290641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q651313$E8F6BAF1-0781-4435-B746-952EEC308A10","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q651313$3985EF9F-A4CB-45E7-947F-A5980A370280","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2c499612d352adb9bf630a964e4498c3cb854f6a","datavalue":{"value":{"time":"+2011-12-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q651313$2D14F30C-BF59-4173-8F0B-7FEAB049DB81","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b5e2d31bb7562716dce76a4ddde10d87fae1c776","datavalue":{"value":"A constructive analysis of the logical notion of satisfiability for first-order intuitionistic formulae is presented. Satisfiability is considered in the framework of the topological semantics. ``Constructivity'' means that the law of excluded middle, the power-set axiom, and the axiom of choice are not used. The main idea is that the semantical notions are treated strictly in the ``constructive'' formal topology theory. The author's considerations are based on constructive proofs of soundness and completeness for first-order intuitionistic logic proposed by G. Sambin and T. Coquand [\\textit{G. Sambin}, ``Pretopologies and completeness proofs'', J. Symb. Log. 60, No. 3, 861--878 (1995; Zbl 0839.03022); \\textit{T. Coquand} and \\textit{J. Smith}, ``An application of constructive completeness'', Lect. Notes Comput. Sci. 1158, 76--84 (1996; Zbl 0852.00045); \\textit{T. Coquand} et al., ``Formal topologies on the set of first-order formulae'', J. Symb. Log. 65, No. 3, 1183--1192 (2000; Zbl 0965.03072)]. Namely, satisfiability of a formula is defined in terms of a canonical topology on the set of all formulas. This notion is characterized also by a syntactic calculus operating with the sequents of the form \\(\\Gamma\\underline{\\vee}\\Delta\\) whose intended meaning is that the conjunction of all the formulas in \\(\\Gamma\\) and \\(\\Delta\\) has a model.","type":"string"},"datatype":"string"},"type":"statement","id":"Q651313$DE21979E-9C42-4177-8ED4-8A3E51572D53","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"b1f73afd33192153e94113807fdc62b87cbaa1ee","datavalue":{"value":{"entity-type":"item","numeric-id":234728,"id":"Q234728"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q651313$E3D40F36-0554-4296-B53E-E4826922656C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q651313$76BB64ED-C5EC-4804-84FA-D6F6512A97A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d971f250f4b60bd91da7e9350568180af141e6af","datavalue":{"value":"03F03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q651313$C9CC8CFB-0A4C-4A06-A0FA-E06E794151CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e5d18442d459f776caea349da745bbaf9554be1d","datavalue":{"value":"03F65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q651313$4E4A52D2-A7E4-4301-B911-CC64C533268C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ead470ebd34acc59be4ea93aa9e35dc4db803efc","datavalue":{"value":"5987965","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q651313$7A22995F-91FC-4941-86AA-64F3E6702614","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q651313$AF4041CE-B8F6-41C9-B386-6A424729E675","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"827b845d5e543bed4cf2f3d0c25bddb70759060f","datavalue":{"value":"topological semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q651313$14216C73-0043-45BF-9DC5-0C3B13C7C9C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"252f9f9ed9fe8ca406cc19fba38a46c0414791ee","datavalue":{"value":"satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q651313$AE209DA6-BA68-40C6-AF24-DE2F241697C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3d7c24935dcad54bb8b35bd2297a2d654d149a5b","datavalue":{"value":"constructivity","type":"string"},"datatype":"string"},"type":"statement","id":"Q651313$F876A214-F305-437D-B7D4-7126E3103C94","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":"Q651313$F50481E4-B398-429A-9CE7-CE8682BD64E3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f79d2fa638aa4642047d89f5ac28c391a44be26d","datavalue":{"value":"https://doi.org/10.1016/j.apal.2011.06.019","type":"string"},"datatype":"url"},"type":"statement","id":"Q651313$0143F56A-3E7E-4FB3-B8E9-F0F44829F424","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"bfb4a6ba6a1801ae29be1978444bfa9fdc10119e","datavalue":{"value":"W2056060841","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q651313$44C5BEDF-7DD3-422C-B60D-63FB50B36D75","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b01a7796542261e07d41a2491f4c7ed1eab0b746","datavalue":{"value":{"entity-type":"item","numeric-id":5448614,"id":"Q5448614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q651313$E96A239F-21B9-4D67-9157-E1AA7445BC7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ef1cb1b59cf439ebb490622011d9effa79bbdc7","datavalue":{"value":{"entity-type":"item","numeric-id":3499749,"id":"Q3499749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q651313$339731CA-D0B2-4BEC-ACE6-1C81F2EF3EC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d07e836c745e9ff71257df133eac37d9ccc626ca","datavalue":{"value":{"entity-type":"item","numeric-id":4527918,"id":"Q4527918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q651313$A71599BE-7854-4B10-800D-B0A830DA26B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c8d0dda71cd4de4005dfe831ab14458886317a6","datavalue":{"value":{"entity-type":"item","numeric-id":4647571,"id":"Q4647571"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q651313$4A4B2986-8413-4B74-9D6C-0B1A51F2AAD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de26bb8ee6b7909c4d8fc4004fd737791e1c9a4e","datavalue":{"value":{"entity-type":"item","numeric-id":3322099,"id":"Q3322099"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q651313$212BD835-D740-4AC9-AFDB-047CD03F0A73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9cb318559b5e8b835fb9fc7ea1d7ddb2a0c1f9c","datavalue":{"value":{"entity-type":"item","numeric-id":5718565,"id":"Q5718565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q651313$E937B5E1-7041-4E03-8BDC-EB53B1DE6FA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"96018a99b8366943bf6654b4677e7e411906125d","datavalue":{"value":{"entity-type":"item","numeric-id":3481701,"id":"Q3481701"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q651313$FA1FE6AF-7933-4ACA-8FB7-E7E2D99003E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a6b93763c3bee209b670cc606716e146a89ae81","datavalue":{"value":{"entity-type":"item","numeric-id":4858821,"id":"Q4858821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q651313$C887FBA6-1B2C-42FB-B144-6D0074108367","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"996dd2d2e697da5035f09f48f7147dd89551ea54","datavalue":{"value":{"entity-type":"item","numeric-id":2575775,"id":"Q2575775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q651313$41EE4BD2-D557-4464-A4F3-B8A86DDE3A23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3652d520789475601e366029ce7b257ab62a1ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5905909,"id":"Q5905909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q651313$FBD0E31C-EDD8-4BFF-9742-648B25578BCA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f472f91b2b729e7508b82ae1ec44fc20d7f80d92","datavalue":{"value":"10.1016/J.APAL.2011.06.019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q651313$398E97A4-6284-4AC6-98C1-F29CC007CE4C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"49d1a9277dfb738fc9db76565150cb370a9a235d","datavalue":{"value":{"entity-type":"item","numeric-id":5448614,"id":"Q5448614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"45fa6bd444c24af8d8b077ba51fc8ec7d13dfad4","datavalue":{"value":{"amount":"+0.7768951654434204","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":"Q651313$02B7FD05-4131-48AF-8386-0DA7D5E9B051","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"543a3124ca08efd7f520ac8b7f1d8d684eb946f0","datavalue":{"value":{"entity-type":"item","numeric-id":2193975,"id":"Q2193975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"55fa4ccb79ebb365c9be87d2824fff05c5d9942b","datavalue":{"value":{"amount":"+0.7706412672996521","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":"Q651313$95555F26-F4E7-42B6-99B9-A1E8EB4507EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f861f4558c48b906a6e52596d355b2e51b454283","datavalue":{"value":{"entity-type":"item","numeric-id":4282610,"id":"Q4282610"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce4fed13b6241a7e0744d2b3b8874a4982b9d27b","datavalue":{"value":{"amount":"+0.7666130065917969","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":"Q651313$96CC85D1-E292-4AC1-B963-07D4257F5931","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"90dc0ffdfd43a44a8ec1748a6e94a6dd8d7a9319","datavalue":{"value":{"entity-type":"item","numeric-id":3755454,"id":"Q3755454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6edf637a70856f03bc664931df0e1727e799988a","datavalue":{"value":{"amount":"+0.7501715421676636","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":"Q651313$36A3BF8F-836D-4ED6-A759-C6F4B351F35A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"30bc8e4a44522e2de7bfc8cabed381b6efa28b5e","datavalue":{"value":{"entity-type":"item","numeric-id":2848884,"id":"Q2848884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56263ff7031ea5f3f49cbe3ed05a9db2ba63c331","datavalue":{"value":{"amount":"+0.7459731101989746","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":"Q651313$EA269FED-EB64-4B27-A3E0-88826BE0672A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A constructive investigation of satisfiability","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_constructive_investigation_of_satisfiability"}}}}}