{"entities":{"Q915716":{"pageid":917564,"ns":120,"title":"Item:Q915716","lastrevid":65350935,"modified":"2026-04-12T01:59:20Z","type":"item","id":"Q915716","labels":{"en":{"language":"en","value":"Satisfiability of formulae with one \\(\\forall\\) is decidable in exponential time"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4152339"}},"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":"Q915716$408D64FC-AC66-43D2-B6CD-0F9A9BD1E034","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4c9520f7ee5a459ac9a3d7e360b927d69246a92c","datavalue":{"value":{"text":"Satisfiability of formulae with one \\(\\forall\\) is decidable in exponential time","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q915716$71DEC498-172A-48FA-9CDD-1D62E6E3AA15","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d7286d10fd3d216cd65f8b28452bee51dd4585e3","datavalue":{"value":"0703.03002","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q915716$622748B4-CE2F-4255-9D7F-508E1AD99098","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5c755a7d206d9dc0b755ba0e516219fb0954519b","datavalue":{"value":"10.1007/BF01651329","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q915716$9A89C5F6-3B4E-44E1-B6FB-18F789ED87B7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d92e5b50a477cfe238ac688c9a8eb0ddc7ad041e","datavalue":{"value":{"entity-type":"item","numeric-id":204638,"id":"Q204638"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q915716$594EA30B-D5C8-4150-B5CF-09F1DB150D2A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a0a7cd28a9f85b9c6ad57bd5bb1ae477bfe37846","datavalue":{"value":{"entity-type":"item","numeric-id":114337,"id":"Q114337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q915716$E2E8AA73-6FAB-4902-8C0D-975D61206F95","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"70d2fbf8bcd48a5ca1ac752985098b379d0dbb65","datavalue":{"value":{"time":"+1990-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":"Q915716$CE782225-2F49-4F87-91C8-F85EEE45209A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f4fcf08102aef114d92b2f02ad00a308505ab2d9","datavalue":{"value":"By predicate logic (with or without equality) the author means first order logic without function symbols. With function symbols present, the author speaks of full first order logic (with or without equality). A prefix class K of formulas is called maximal solvable if it is solvable (i.e. satisfiability for formulas in the class is decidable) and if every prefix class which properly extends K is unsolvable. As set forth by the author, the satisfiability problems for the four maximal solvable classes in predicate logic (without equality, \\([\\exists^*\\forall^ 2\\exists^*]\\) and \\([\\exists^*\\forall^*]\\); with equality, \\([\\exists^*\\forall \\exists^*]\\) and \\([\\exists^*\\forall^*])\\) are NEXPTIME-complete. The author proves that in full first order logic without equality the satisfiability problem for the unique maximal solvable prefix class \\([\\exists^*\\forall \\exists^*]\\) is dedicable in deterministic exponential time (EXPTIME). In another paper he shows that in full first order logic with equality the satisfiability problem for the unique maximal solvable class \\([\\exists^*]\\) is NP-complete.","type":"string"},"datatype":"string"},"type":"statement","id":"Q915716$5EF6CC84-1695-4C91-905D-03A1E8BC4172","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q915716$5DF0AA03-76A3-4E27-BDFB-9067CDC19C74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q915716$883E3751-A8E5-4757-BC2F-3A00E7D7AB5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b4346faa01bb5fb0576370374d6456afd58d5666","datavalue":{"value":"68Q15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q915716$1B517227-E7B1-4BFC-9BC7-468EAC27B338","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d7656d1c841701431b0b3d99d23720089a267cbb","datavalue":{"value":"03D15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q915716$9C23D615-514A-4D1D-BEBA-8867481118ED","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0a02a5b58efe5fd98f82d415bb8b4ea985087fe7","datavalue":{"value":"4152339","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q915716$04984E3D-C5F9-4869-ABB1-100017296093","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6c728a3409a7e6cbc832749e3fd032e6079ab059","datavalue":{"value":"quantifier prefix classes","type":"string"},"datatype":"string"},"type":"statement","id":"Q915716$FF185A60-08D6-4935-92D9-0EF3B71048E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"777b109c653c621c98ae209c292e362646b61f2f","datavalue":{"value":"first order logic without function symbols","type":"string"},"datatype":"string"},"type":"statement","id":"Q915716$644BBC32-14A5-4992-975E-228BEF35F4A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a97e4ada12d0b713975990d9d7c87480868ed04a","datavalue":{"value":"full first order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q915716$B8C823B9-0C7B-4E63-B336-F3A235D9ABB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bfded98921fb7d9cf722f229333546d869ef30c7","datavalue":{"value":"satisfiability problems","type":"string"},"datatype":"string"},"type":"statement","id":"Q915716$7EE247ED-68AD-4034-B91A-3A0316156C5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"71dfff84f8cc5e741756fa09a4cff5ebdf3ec079","datavalue":{"value":"maximal solvable classes","type":"string"},"datatype":"string"},"type":"statement","id":"Q915716$A25E872C-A61E-42CB-81B9-DF2860D6C51A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"47ffb11d311f15e75105378f70577a0fb9401923","datavalue":{"value":"NEXPTIME-complete","type":"string"},"datatype":"string"},"type":"statement","id":"Q915716$AB624B34-8C64-4350-921C-3D9D7D5C468A","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":"Q915716$50EA74B7-55C4-4DDE-B332-73179C1C8DCC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"648af4444efef3dfface63422920536bd2b0c180","datavalue":{"value":{"entity-type":"item","numeric-id":3928246,"id":"Q3928246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q915716$28B5C161-B12E-4FBD-A439-8D8EEC41685F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5369245c683380663d43367502a396b591af1be3","datavalue":{"value":{"entity-type":"item","numeric-id":5763293,"id":"Q5763293"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q915716$CB3BF59C-AED6-4479-8B21-168F809156C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc87ad8b718d652fb612db8e727345bcdad12278","datavalue":{"value":{"entity-type":"item","numeric-id":3695253,"id":"Q3695253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q915716$8E83FF4E-24F4-486C-926E-F745FD9A7F9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4fab33777dce654ec72e44fec3119c509ea0bece","datavalue":{"value":{"entity-type":"item","numeric-id":4106190,"id":"Q4106190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q915716$DD35284F-E923-4978-B39D-C43996424601","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eda2db14c950cfacb2d9bab387b35d1aadfc67b0","datavalue":{"value":{"entity-type":"item","numeric-id":3284606,"id":"Q3284606"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q915716$15A65A73-CB69-4197-A25C-A8D4BC1CFC02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b051bb91a42a31736fdd8d09157004cdcec793d8","datavalue":{"value":{"entity-type":"item","numeric-id":920075,"id":"Q920075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q915716$D9717416-6C0E-4C55-8265-EA9BEB212AEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d6e5a2ec66a572177ef7c34d7ff9e3c5a3050d5","datavalue":{"value":{"entity-type":"item","numeric-id":1157324,"id":"Q1157324"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q915716$505B3FB4-85F5-4C27-82F3-53D11D78B8AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fb01053f812b841e1e43f0b05c416be3c7a6c318","datavalue":{"value":{"entity-type":"item","numeric-id":5802125,"id":"Q5802125"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q915716$048AAFEB-CD9C-46F3-8E41-952F1357CE59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1613a6ff5ac7b010de5ba58e55ebd9cdec3d5273","datavalue":{"value":{"entity-type":"item","numeric-id":5765445,"id":"Q5765445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q915716$199EF6B0-248E-474A-893C-7330BCBCE6F6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"eabd6d404d830cf67717c1da1eec72c9cecd7ba4","datavalue":{"value":"https://doi.org/10.1007/bf01651329","type":"string"},"datatype":"url"},"type":"statement","id":"Q915716$A3B731B2-C95E-4D81-AC33-E4671F4561F1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"55cce6447ed03fb3e1c701c833b79196c2586478","datavalue":{"value":"W110461417","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q915716$27A2F579-DF07-475D-9E28-27741F935FF1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0af0f1beb39946bafec9509d7e34ecb9867e2653","datavalue":{"value":{"entity-type":"item","numeric-id":3348901,"id":"Q3348901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fdc6178a370dc5dfef5eacdc02cc07c4e16ce6c4","datavalue":{"value":{"amount":"+0.8294572234153748","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":"Q915716$03BD367B-7525-49D3-B471-9850149B5C61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b4da257adfa3098e146111db07027c7417c2813","datavalue":{"value":{"entity-type":"item","numeric-id":4731176,"id":"Q4731176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3b32dec6392d087ca29f0cda45fabe2a262f8b49","datavalue":{"value":{"amount":"+0.7910223603248596","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":"Q915716$26876786-0E01-44BF-A433-BE7C7C4B9EDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"73da5313fd295be75d1eb7646a11271e625a3d6a","datavalue":{"value":{"entity-type":"item","numeric-id":4002871,"id":"Q4002871"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5a25a4f8a708fc8aba89be08d9dc27b5d8d39329","datavalue":{"value":{"amount":"+0.7817167639732361","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":"Q915716$33BCF7A9-D383-437E-A276-913F75929C2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8dfe26a710ada800ab72a0ca14c6bf5d770124e7","datavalue":{"value":{"entity-type":"item","numeric-id":4868240,"id":"Q4868240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2730ebb6434afbeba661c9d37ac532618415d4de","datavalue":{"value":{"amount":"+0.7788846492767334","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":"Q915716$E7873B12-4692-45BB-A48B-75F344A3C585","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"77a7e00159c0998cc84e46c278f0342852cd31ac","datavalue":{"value":{"entity-type":"item","numeric-id":800915,"id":"Q800915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cde9e4e0cd1b93779f1eed02f0d87ebfcdc75992","datavalue":{"value":{"amount":"+0.770979106426239","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":"Q915716$C40B73D6-3217-472E-9859-DAD2FF97B7AE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Satisfiability of formulae with one \\(\\forall\\) is decidable in exponential time","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Satisfiability_of_formulae_with_one_%5C(%5Cforall%5C)_is_decidable_in_exponential_time"}}}}}