{"entities":{"Q2751362":{"pageid":2762101,"ns":120,"title":"Item:Q2751362","lastrevid":47693950,"modified":"2026-01-02T11:11:22Z","type":"item","id":"Q2751362","labels":{"en":{"language":"en","value":"Equality reasoning in sequent-based calculi"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1664649"}},"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":"Q2751362$A57F59CB-9CCF-4D1F-9477-ED5431A6C275","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9e341c349167ae33669e6461b27f507b4d865125","datavalue":{"value":"1011.03004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751362$EBF2E4ED-A213-4FE5-9990-48EC63BC17CE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8267b3be2b739476dcf61b4c89d4f97117c42016","datavalue":{"value":{"entity-type":"item","numeric-id":671658,"id":"Q671658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2751362$95BC9799-593E-470A-A030-B998FBEEED5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bab2dfee53655d9cc8087a652185465cb178825e","datavalue":{"value":{"entity-type":"item","numeric-id":229754,"id":"Q229754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2751362$D949CF4C-2D99-42DB-9D82-14458C20AA99","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"da39a7fd1a76a539516fc1c6fcfdf3ed355f9814","datavalue":{"value":{"time":"+2002-07-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2751362$0CBA50DC-91B6-499C-9CF7-4FD72623155D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751362$1D54253F-BA91-4D7B-B7E7-AF6B0AD59175","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751362$850EE0D2-C9AD-4A78-8D61-EBF954A2B1E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"89663cdc2c9f64b2cd0a104bcac86329d89b9b2d","datavalue":{"value":"03-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751362$73991282-895C-4A44-9663-235940AC2CD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24aafcf24a21bd70cd3b62d3f5f72a6d0d82d816","datavalue":{"value":"68-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751362$AC969E36-99C7-4942-A830-AB0C3DC8F56B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"465dc34eb2e42ec66e19ea8c83b2d229b053b330","datavalue":{"value":"1664649","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751362$A3E31BCE-CBE5-4C9A-812F-C80A832A0F20","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"421a43f4b0e8832a026eaa34353c95869f115bee","datavalue":{"value":"survey","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751362$BA2AEB38-3F7F-44B0-B111-784E1BF64558","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"18e01ecce4df8c78dfb2394193651f3c03479d74","datavalue":{"value":"sequent-based method","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751362$E2CAFBE3-3CC4-4B40-A822-1B3C1478E8C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751362$72869794-40AB-4D03-A5BC-43354044951A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8b8a9646b82dbeb50d8df2be83409261d3b2042d","datavalue":{"value":"proof-search","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751362$4293A583-4B28-4466-B4ED-2639951E285D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8880533df93c347546f078adfcc714520827999e","datavalue":{"value":"translation of logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751362$EDE41C92-CB28-4340-9D18-4F90A2C51401","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751362$8C2326E4-30FE-4D55-B1CD-675D1B488397","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f5c6032cef5106a349fb58e5521f10e0d25e77b","datavalue":{"value":"simultaneous \\(E\\)-unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751362$C9BE4561-2B1C-438A-8027-33497207CBA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d120f16a4a449e17abe99fcf1fc6dfa592e9035c","datavalue":{"value":"tableau calculi","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751362$F45D6663-852F-49A3-AC2C-C1FDF0875EB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"70d96809292a87cd8b7062928a512b45a735782c","datavalue":{"value":"equality elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751362$D70EC592-47A2-435F-AC40-57490A296D1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ed89bf91967dd7c6a7c8ea4f7c58086c35c0930","datavalue":{"value":"equality reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751362$AF559123-314A-46DC-9BAD-ADA5C699B898","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"75628edfe18d9271975b72a8a7ded77f899517f2","datavalue":{"value":"nonclassical logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751362$CF4D1A93-B1C2-488C-B503-BD035C090FE3","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":"Q2751362$4755F980-DA1F-4C36-BFEA-0F9FE946B1FA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ff955d2e49783c8be1e06b55be2cd392f4a1f558","datavalue":{"value":{"text":"Equality reasoning in sequent-based calculi","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2751362$42F28967-FD29-45A6-9D8D-510590C73492","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"96a2e6a24717d72847475d2f80cb808404c20c6b","datavalue":{"value":"The authors present a review of automated reasoning techniques for all main sequent-based methods of automated reasoning. The paper covers the following topics: NEWLINENEWLINENEWLINE-- methods of proof-search in sequent-based calculi, NEWLINENEWLINENEWLINE-- translation of logic with equality into logic without equality,NEWLINENEWLINENEWLINE-- theorem proving using simultaneous \\(E\\)-unification,NEWLINENEWLINENEWLINE-- tableau calculi with rigid paramodulation and superposition,NEWLINENEWLINENEWLINE-- the equality elimination method,NEWLINENEWLINENEWLINE-- equality reasoning in nonclassical logic.NEWLINENEWLINENEWLINEThe paper contains a voluminous bibliography concerning the considered topics.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751362$6BAEE832-FB8C-4018-87E8-23272A41657B","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"05f3dff3edc7d97b14af7ecb326f488fb3fee31b","datavalue":{"value":{"entity-type":"item","numeric-id":583186,"id":"Q583186"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2751362$5A346DD0-1529-485A-8B64-625B007145AF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"060de0ddd0b0ab988fb6156915a646e42e8f6dc7","datavalue":{"value":{"entity-type":"item","numeric-id":2785839,"id":"Q2785839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9810548423288aa32d82f754fa99c5f3c24fbd83","datavalue":{"value":{"amount":"+0.7641947865486145","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":"Q2751362$9007FD6F-E7FC-4D0F-8017-FD81EDA37C40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9139f6ceedbc79a8c36ce64cb3447ce439e96552","datavalue":{"value":{"entity-type":"item","numeric-id":5394604,"id":"Q5394604"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2fe4c80a4fd61c6ffc55351f558dc2519dbb9281","datavalue":{"value":{"amount":"+0.7641938328742981","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":"Q2751362$9FAED1ED-B4C7-485A-9A75-D2A509E40F49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"516c0d9ade4668ccaad1376068843547fa30bd7c","datavalue":{"value":{"entity-type":"item","numeric-id":5901869,"id":"Q5901869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78555cb715be501663d801ecd84eb35a132b738b","datavalue":{"value":{"amount":"+0.7542800307273865","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":"Q2751362$C491E81E-45D0-4090-8C66-9EA2251FEDF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4564dcbe209d24a2f509e63518773f769d6b6c9e","datavalue":{"value":{"entity-type":"item","numeric-id":4524792,"id":"Q4524792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"00cd76622d583f6c303d9a16474fc81f4ed21dcc","datavalue":{"value":{"amount":"+0.749461829662323","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":"Q2751362$4B67DC4E-4779-47A2-95E1-57787B11B5CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c86f80878e3d6987e2d89acaf5e00e9e68411b0e","datavalue":{"value":{"entity-type":"item","numeric-id":5698235,"id":"Q5698235"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"00cd76622d583f6c303d9a16474fc81f4ed21dcc","datavalue":{"value":{"amount":"+0.749461829662323","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":"Q2751362$6865C6EC-5DEB-4282-9D03-B7B30D2E6288","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2751362","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2751362"}}}}}