{"entities":{"Q1185455":{"pageid":1196204,"ns":120,"title":"Item:Q1185455","lastrevid":70220439,"modified":"2026-04-13T13:16:10Z","type":"item","id":"Q1185455","labels":{"en":{"language":"en","value":"A resolution framework for finitely-valued first-order logics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 38436"}},"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":"Q1185455$647B15B8-FC3F-423E-A7E4-296DCC7E1061","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"869c6bf6453057a0582cb59f1e258650b63d0c73","datavalue":{"value":{"text":"A resolution framework for finitely-valued first-order logics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1185455$DF8F0EC8-0C45-4AC0-B2EF-E3E21D86E72F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6424b8c92b4333ad91c9187a1b91152a28e0b288","datavalue":{"value":"0751.68062","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1185455$3477C77B-AAA2-4337-B44C-BD77B6D1AC43","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1480ff168fb94e11febcf6c36230f57ff61655b4","datavalue":{"value":"10.1016/S0747-7171(10)80002-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1185455$81264541-9295-45E2-A920-F932AA36568B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7c4e228a29afeb420d031832419eeb44a6dbdbe7","datavalue":{"value":{"entity-type":"item","numeric-id":736796,"id":"Q736796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$2FC8FD05-2C85-4345-A7E2-5F1768983D18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"eb51d0f7231631be2c151ca0e23437f5ddb283b3","datavalue":{"value":{"entity-type":"item","numeric-id":687162,"id":"Q687162"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$BAD1F5FD-D818-48E6-8179-8F1DE678EE9A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$BDE91229-4C84-4A2A-940E-B26CCA380A41","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"120787504bea9565def539fb4bfb19084956028b","datavalue":{"value":{"time":"+1992-06-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1185455$CC74CF56-FA72-4641-935D-605D1437B530","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"3c0f3bce790b54a15c7404872985ef2bcc510869","datavalue":{"value":"The authors outline a theoretical foundation for the introduction, analysis and implementation of resolution proof systems for finitely- valued first-order logics (FFO logics). They base their approach on the unification of the algebraic theories of logical systems and non-clausal resolution. Thus rich algebraic techniques should be at hand to express and investigate metatheoretical properties of resolution proof systems for FFO logics.   First the notion of a resolution proof system for a first-order logic is introduced that generalizes the concept of a non-clausal resolution proof system for a propositional logic elaborated by the authors elsewhere and the resolution proof system for classical predicate logic developed by Manna and Waldinger.   The proof that every FFO logics can be formalized as a resolution proof system entails the effective constructability of FFO resolution counterparts from the semantic descriptions of these logics. This sets the stage for an automated generation of theorem proving environments for FFO logics.   At last two speed-up techniques, the set-of-support strategy and the polarity strategy, are examined to render the theorem proving system more effective. These techniques are to direct and restrict the application of the inference rules.   It is demonstrated that both strategies preserve the refutational completeness of resolution proof systems.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1185455$BAE5869D-F1FC-4853-A895-9AFD17697F0D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1185455$94774858-4A76-4151-9CD4-C950C8A807D9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"818b135590f2218abe4e1d756b4de944c0648b51","datavalue":{"value":"38436","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1185455$9D49F666-390B-442B-8AEC-1256B119135A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1185455$384C3BDD-6C24-416A-BCEA-5BBA6CEDB0D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"49d0d4f6ec68fa6ad5925f0339571a99e57662b4","datavalue":{"value":"finitely-valued first-order logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1185455$6A048B9A-810F-4827-A5E4-1A015C047378","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"14a0dd3e1b83404196449aa90cc83aae915af1cf","datavalue":{"value":"proof system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1185455$F690ECC8-ABF3-4290-B319-477FB9D1AAA0","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":"Q1185455$A41F8579-3CBA-4EF9-A279-794A9292C5C8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2747d10da3351289d1b17c903ad4959bea6af896","datavalue":{"value":{"entity-type":"item","numeric-id":3030268,"id":"Q3030268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$816A496B-ADAC-433E-B301-7D7A72F22950","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5a3768f9178495dd2a65db2685e2dc39f9eef9b","datavalue":{"value":{"entity-type":"item","numeric-id":3206928,"id":"Q3206928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$0EA6173C-D6F2-4073-950C-46114D989BE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c946937d28c3cb40d97cc7256024ccadedf80fa2","datavalue":{"value":{"entity-type":"item","numeric-id":1104915,"id":"Q1104915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$37968D48-6D3D-46B8-9C93-20DA7EE563DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f71c78fa37d89de9f639230f926e61413cb8289","datavalue":{"value":{"entity-type":"item","numeric-id":3800001,"id":"Q3800001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$BC6DFAEF-5EA9-4A84-9D59-F0DA032DA56C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e69a1b0696d3d19ee0dc3aad945f1b6fcdf0a0b7","datavalue":{"value":{"entity-type":"item","numeric-id":3792274,"id":"Q3792274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$E972B412-51DF-4C5C-89BA-9D05857BA702","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9bb2c5c854e8d8056e258c4498ee6678adbf39d8","datavalue":{"value":{"entity-type":"item","numeric-id":4189255,"id":"Q4189255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$DE521A05-6F8A-42B4-AE41-2ED6C2E7979D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fae58cabc6210877500b69d67f8a52d2647519a6","datavalue":{"value":{"entity-type":"item","numeric-id":3268305,"id":"Q3268305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$8A5349AE-713C-43DB-A687-BCB1DB03D880","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"63ad2ed6b7262bc4aaf760dd16acb7d192abb88c","datavalue":{"value":{"entity-type":"item","numeric-id":3777497,"id":"Q3777497"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$9BE06E33-29FA-4ABF-A1FD-3722FA7E751A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7add01291c95ebcb031afac6fc8c8b1659115c10","datavalue":{"value":{"entity-type":"item","numeric-id":1229761,"id":"Q1229761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$DE2EC077-D15C-4E31-88CF-CF7DEB3F7CE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3caa88058b79599cc58c0a1d5cb3b4529602ee33","datavalue":{"value":{"entity-type":"item","numeric-id":4121876,"id":"Q4121876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$5F92CFDC-24BE-4A57-95A0-5505FDB409F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1a8c1250dbca5a1914c2e0ccc1c1670d1eb9d18","datavalue":{"value":{"entity-type":"item","numeric-id":1157923,"id":"Q1157923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$9594DCB0-B409-4F9B-BF47-AB583EE77EF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bade6a36335738f89d892b702a4106b53a340bf1","datavalue":{"value":{"entity-type":"item","numeric-id":3791114,"id":"Q3791114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$6C2DCCA3-D5F2-4F49-9611-051E5827EA83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a76cbde9dd05d527c97cc033a7687dee65f2bc83","datavalue":{"value":{"entity-type":"item","numeric-id":3714047,"id":"Q3714047"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$6149707F-26B2-4EAC-A72D-17A72C431929","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7763f870fd431b4577b4a07d2469375f7ba20f0c","datavalue":{"value":{"entity-type":"item","numeric-id":3972030,"id":"Q3972030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$1CB22A1B-F69A-4BF0-8BB3-107ACFDB2393","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d855aedb6b8689008dfa235ba2981fd83a136c50","datavalue":{"value":{"entity-type":"item","numeric-id":5661846,"id":"Q5661846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$16AE73BD-139D-46FB-AEE1-BDA2939350EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19b6db54ea89d2d92e7b3ac7acefa676a1537b39","datavalue":{"value":{"entity-type":"item","numeric-id":3786473,"id":"Q3786473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$09230D64-3AE5-4B94-82D0-425C574017B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a39eb133f0e503c3b7de1a9d3f53f5823701a20","datavalue":{"value":{"entity-type":"item","numeric-id":3999204,"id":"Q3999204"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$E101D7F9-1145-4A4A-942F-21F9C8D50D18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5d5e20d299ace830b10417c44478fbe5460fdb6","datavalue":{"value":{"entity-type":"item","numeric-id":5748907,"id":"Q5748907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$698CA251-3A0B-4683-9DE3-6803F00E6040","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d648b3bf1fdf53081e71a35066dfc48abd45f8fd","datavalue":{"value":{"entity-type":"item","numeric-id":4273485,"id":"Q4273485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$D2E1E16D-C569-40CF-B2BE-DE9EB65BFB2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"606b1a2447b57478a7f07c4e89f918f5f3a4eb61","datavalue":{"value":{"entity-type":"item","numeric-id":3485886,"id":"Q3485886"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$40A0618A-2F35-4CEB-A809-CB18A73D7E07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8892c61cc6f9ed6d01929cd49bd2974ceab500e7","datavalue":{"value":{"entity-type":"item","numeric-id":2561584,"id":"Q2561584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$F9A1C3A4-4BE7-4C8E-9F93-99AA352B9DDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0620e875ace4454552471ddc26f3c19b333694a","datavalue":{"value":{"entity-type":"item","numeric-id":3994754,"id":"Q3994754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$1E6FC785-C1E7-4A4F-B9A3-16FECC81A14B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47bab4f7d1b2661e9a9ca3ddc35e5a57311ad582","datavalue":{"value":{"entity-type":"item","numeric-id":5507985,"id":"Q5507985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$ED204729-E869-4089-9784-216ADCFFDF51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"11b6f231eb024fbb0248b8ea953dad94e2ed45be","datavalue":{"value":{"entity-type":"item","numeric-id":5507984,"id":"Q5507984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$A8351591-C435-4D3A-A729-E0B0C434D9F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"abbcbbe97f24f82950314edc7c6f712b067fe22e","datavalue":{"value":{"entity-type":"item","numeric-id":1188523,"id":"Q1188523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1185455$16852026-445E-4ADA-AB70-10147FFB6574","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6021f70475ec456907b1059df7b91dfa79a09357","datavalue":{"value":{"entity-type":"item","numeric-id":1897558,"id":"Q1897558"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ad9ead60c17a2fd9f257aa750eecb218d64aa5e","datavalue":{"value":{"amount":"+0.8034337162971497","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":"Q1185455$992B258F-EC72-460B-87BB-6CDB958D8CAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cdec01f3c91c07e4dbdf899aff373f49d6439131","datavalue":{"value":{"entity-type":"item","numeric-id":1187026,"id":"Q1187026"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e9131939cc7430641f76d6aeba811841158eef3c","datavalue":{"value":{"amount":"+0.8020102977752686","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":"Q1185455$574EA253-638F-47AD-A2A8-12303353677A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"48a3d434253ed919faa661b14e883ac27b635cfa","datavalue":{"value":{"entity-type":"item","numeric-id":2751353,"id":"Q2751353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b7b550ef50f1f68e75ea2f4b75cba7bb37d0b06c","datavalue":{"value":{"amount":"+0.7998285293579102","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":"Q1185455$25608869-F4BA-4A31-A94D-ECCF202CFD18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3c9e9751b2f626072990ed5ebb4122586aea839","datavalue":{"value":{"entity-type":"item","numeric-id":3976578,"id":"Q3976578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0f7edd9adac60caa74e628e76f09915ee8e5ee0c","datavalue":{"value":{"amount":"+0.7989981174468994","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":"Q1185455$982A3DFE-1BE4-4A6E-B3EF-9B37C0DE08F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f9cc9840145fafc0b23cf70f78d0ed48128753f7","datavalue":{"value":{"entity-type":"item","numeric-id":4881605,"id":"Q4881605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b376696016cebdfdccfd7a80fd2258e02eb50220","datavalue":{"value":{"amount":"+0.7898091077804565","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":"Q1185455$4D91F236-EADC-470B-8C0B-C1BE4FD892EE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A resolution framework for finitely-valued first-order logics","badges":[]}}}}}