{"entities":{"Q1904405":{"pageid":1915147,"ns":120,"title":"Item:Q1904405","lastrevid":74254449,"modified":"2026-04-14T19:12:27Z","type":"item","id":"Q1904405","labels":{"en":{"language":"en","value":"A note on assumptions about Skolem functions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 828198"}},"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":"Q1904405$25652AB4-93D9-4E17-B690-DA46C93CB93C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"924b9184f1249fa6c3710ce4d1a8c7d20c23fab9","datavalue":{"value":{"text":"A note on assumptions about Skolem functions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1904405$7A3A1FEB-B290-4CD0-98AB-DFC2EEEFF09A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0edbc9d57eeb2b463ca87054b96ccad8aa71cf0e","datavalue":{"value":"0879.03006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1904405$6CEB2D80-A870-4527-B03F-A5205E6BAAF6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"536ddfb62e1bcd41393bb4b271c8a94115f1d2ad","datavalue":{"value":"10.1007/BF00881919","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1904405$42527A28-3B15-4E45-84A2-F469EF7344FA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e858e644a5f8f9e799cff3da307c11b687abc60c","datavalue":{"value":{"entity-type":"item","numeric-id":831914,"id":"Q831914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1904405$18593554-EDBD-49FD-AE6E-B734A1B20B01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8ad85fd0db6467d71e74313095d444d398003ebc","datavalue":{"value":{"entity-type":"item","numeric-id":1097715,"id":"Q1097715"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1904405$31D343B9-8C17-437F-9E43-E85A2083ADC0","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":"Q1904405$47D0FCF2-C502-43B3-A139-CD0AB42A7C37","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c6a4059c7dcb0f47b5fff19f8c6a086d332c3ac5","datavalue":{"value":{"time":"+1995-12-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1904405$6CAFE7D1-6CE1-4E71-A93B-45D7DCD268B6","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"229e0fabe33401b28dc2acb7d15d2bb14dd756fa","datavalue":{"value":"The paper presents a sharpened Skolem theorem for first-order logic. This optimized skolemization technique does not produce an equivalent proposition, but it preserves satisfiability, which is enough for its use in refutational automated theorem-proving . This optimized skolemization can be decomposed into a transformation of the proposition to be refuted, followed by a standard skolemization. It generalizes optimized skolemization techniques known in special fields such as many-sorted first-order logic and modal logic.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1904405$6BC897F1-F725-4254-ACCE-FBCEBF8A2C6F","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"085e1d1d24be02ea23effd8a6c73fa275fc02f04","datavalue":{"value":{"entity-type":"item","numeric-id":436401,"id":"Q436401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1904405$54629D5B-0A00-4D09-81A7-33C56779912B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1904405$DA787554-1ABF-44E8-A2E2-FE075686D1E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1904405$76AECA8C-F23A-4A0C-B145-3640F82A5D4A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0dc6a1ec85f9c7e7cb14176882c4e213242911f5","datavalue":{"value":"828198","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1904405$23143002-1023-458F-993C-622AA3A8F18D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"43500ab12b3512a8fae708070fe1439bd0ade508","datavalue":{"value":"preservation of satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1904405$3349D39D-854B-4880-B2E5-64FD0F88D496","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"467ec96bb7f54f53140e0bc6e61095754be25d9b","datavalue":{"value":"sharpened Skolem theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1904405$8A5A8C2E-2BDF-4BD4-BBED-2C7F42510425","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2e80a7123e4ea6d0418cb24d37b1837f13e3514","datavalue":{"value":"first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1904405$ED8BE032-E0FB-4C26-8A41-A2BE0BF7FAB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ed7e6e9c94ff3b60db290c50ec042b595f810759","datavalue":{"value":"refutational automated theorem-proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1904405$CD1E9CB4-4A22-4706-996D-9A553402560E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6f9585b668c516d22f035ea31ed7d88390e0cd8d","datavalue":{"value":"skolemization","type":"string"},"datatype":"string"},"type":"statement","id":"Q1904405$CDBA56D0-48CD-4149-BE43-5273A8960EDF","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f63de557d279c4616add6af7fb4f5f08e4cbf484","datavalue":{"value":{"entity-type":"item","numeric-id":41399,"id":"Q41399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1904405$98C0AE14-0835-42CB-A8B4-96814BB753BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1904405$17C6874C-C47C-4156-8573-AE2D0C1EF4BB","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":"Q1904405$9F2F76DD-AE75-477C-8D1B-B5C4BC4BF571","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7ac3d7ec2b15acefd0efec27878eb9b4d230b02","datavalue":{"value":{"entity-type":"item","numeric-id":3867808,"id":"Q3867808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1904405$596E2764-3776-4B2A-B244-88ED4BAC5FFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1aa9e8bb4ef37ec285d6c238c3f5aa5ed5c9a38","datavalue":{"value":{"entity-type":"item","numeric-id":4139711,"id":"Q4139711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1904405$47E16440-EAA9-48DA-8E90-6FF70315BFD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f74512d1738c9d1ad87a430c2d90edb232ca525b","datavalue":{"value":{"entity-type":"item","numeric-id":3983938,"id":"Q3983938"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1904405$A133297C-04DD-461F-861D-BBDF6BB70AA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5587664e371fa7cdb52e3b1329f22cf9fcff022","datavalue":{"value":{"entity-type":"item","numeric-id":1101242,"id":"Q1101242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1904405$F9C10953-1109-44D1-BB97-926156851886","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0019d907973d7569cdd61ec3c8c4f916896acc5b","datavalue":{"value":{"entity-type":"item","numeric-id":1801289,"id":"Q1801289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1904405$8F957674-17F1-4C56-80B2-CD2DBF143220","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a177420faefcfce6396fc744cae98a5ec9b03f8","datavalue":{"value":{"entity-type":"item","numeric-id":3992821,"id":"Q3992821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1904405$8CAB037E-0ECD-43B5-8758-8E1A43585C01","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"91accd41c4799a760151929a3853609f56cdd061","datavalue":{"value":"https://doi.org/10.1007/bf00881919","type":"string"},"datatype":"url"},"type":"statement","id":"Q1904405$4126FA55-E5D5-4F30-A284-A2AB1ED9CE82","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e142d3934e425d6082cb95cf4e43967f24c81da2","datavalue":{"value":"W1972410746","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1904405$9BA19191-A6E4-4690-AC0E-D59A9FE74334","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d221f1c51313cd2e2190b3515617e2e06bc27fc3","datavalue":{"value":{"entity-type":"item","numeric-id":5851151,"id":"Q5851151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bcadd249770d5597f97a13edc501d8d41f2687f3","datavalue":{"value":{"amount":"+0.8061840534210205","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":"Q1904405$FF00A683-FF52-4C89-9EA7-CB586A8618BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3625139a48b1b52c210c022004deeddfe4a39cfb","datavalue":{"value":{"entity-type":"item","numeric-id":3122078,"id":"Q3122078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ffc00395cabed03fef259e763c2dbee5a3fb692e","datavalue":{"value":{"amount":"+0.7970210909843445","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":"Q1904405$0CDCD0C7-C0E8-4317-982C-77429088B262","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f279695707abece815dff4d1bf3061f6cd0b08c4","datavalue":{"value":{"entity-type":"item","numeric-id":2879139,"id":"Q2879139"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"96b09f147f69362ef64503c648a298f14646463b","datavalue":{"value":{"amount":"+0.7800504565238953","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":"Q1904405$09435C33-9616-4B01-93EB-DD3F8288EBBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4c05ff52b80d6dbfd5dc36ac59d953a7f881a330","datavalue":{"value":{"entity-type":"item","numeric-id":4304753,"id":"Q4304753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f8c183968c0ea447862411df139d6fb2fa749fb4","datavalue":{"value":{"amount":"+0.7565498352050781","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":"Q1904405$2D1E3E0C-BA57-46CD-8285-23870DE55508","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e8fad119391ac0650fa8016c1ceba6481f2374b2","datavalue":{"value":{"entity-type":"item","numeric-id":3777987,"id":"Q3777987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8d64d1378e3cbe735537086964c27f4c3213df54","datavalue":{"value":{"amount":"+0.7482725381851196","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":"Q1904405$F82068D6-56DA-4E4F-B24D-766AFD792138","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A note on assumptions about Skolem functions","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_note_on_assumptions_about_Skolem_functions"}}}}}