{"entities":{"Q1967066":{"pageid":1977808,"ns":120,"title":"Item:Q1967066","lastrevid":72071394,"modified":"2026-04-14T02:28:08Z","type":"item","id":"Q1967066","labels":{"en":{"language":"en","value":"Automated deduction in classical and non-classical logics. Selected papers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1412344"}},"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":"Q1967066$D460B455-F498-45BC-B7A5-F91408E22A5A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b19898be439025e98b7800c0cf40db7101fca062","datavalue":{"value":{"text":"Automated deduction in classical and non-classical logics. Selected papers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1967066$FFC39248-7433-405F-A588-C4167B4C7749","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ebc8c51189cafe96d52789d1f3f06f96cc1138e1","datavalue":{"value":"0933.00012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1967066$4A4CB6A2-DF9F-4F9D-BE55-C5EC7AD9F609","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7da89d0ee7b7073a01d4628e27e52baa84db71c8","datavalue":{"value":"10.1007/3-540-46508-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1967066$53B6B035-3E20-4A44-97ED-008BBE7DB8AB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1967066$0970247B-C488-4625-934B-B8BB156C88B5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"284fc9f3df76f3601dedbdc5ed75b5473a78563e","datavalue":{"value":{"time":"+2000-03-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1967066$05F045E3-5DF1-474B-B33C-691066855B72","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"094d38404682435587f4801cfca55581057a8df8","datavalue":{"value":"The articles of this volume will be reviewed individually.  Indexed articles:  \\textit{Dowek, Gilles}, Automated theorem proving in first-order logic modulo: On the difference between type theory and set theory, 1-22 [Zbl 0960.03008]  \\textit{Fitting, Melvin}, Higher-order modal logic -- a sketch, 23-38 [Zbl 0955.03030]  \\textit{Kapur, Deepak; Sivakumar, G.}, Proving associative-commutative termination using RPO-compatible orderings, 39-61 [Zbl 0963.68089]  \\textit{Leitsch, Alexander}, Decision procedures and model building or how to improve logical information in automated deduction, 62-79 [Zbl 0966.03011]  \\textit{Plaisted, David A.; Zhu, Yunshan}, Replacement rules with definition detection, 80-94 [Zbl 0963.68194]  \\textit{Boy de la Tour, Thierry}, On the complexity of finite sorted algebras, 95-108 [Zbl 0964.08007]  \\textit{Cantone, Domenico; Nicolosi Asmundo, Marianna}, A further and effective liberalization of the \\(\\delta\\)-rule in free variable semantic tableaux, 109-125 [Zbl 0955.03014]  \\textit{Cantone, Domenico; Zarba, Calogero G.}, A new fast tableau-based decision procedure for an unquantified fragment of set theory, 126-136 [Zbl 0955.03015]  \\textit{Dahn, Ingo}, Interpretation of a Mizar-like logic in first order logic, 137-151 [Zbl 0960.03007]  \\textit{Demri, St\u00e9phane; Gor\u00e9, Rajeev}, An \\({\\mathcal O}((n\\log n)^3)\\)-time transformation from Grz into decidable fragments of classical first-order logic, 152-166 [Zbl 0956.03026]  \\textit{Ferm\u00fcller, Christian G.}, Implicational completeness of signed resolution, 167-174 [Zbl 0962.03008]  \\textit{Formisano, Andrea; Omodeo, Eugenio}, An equational re-engineering of set theories, 175-190 [Zbl 0955.03016]  \\textit{Hustadt, Ullrich; Schmidt, Renate A.}, Issues of decidability for description logics in the framework of resolution, 191-205 [Zbl 0955.03018]  \\textit{Pichler, Reinhard}, Extending decidable clause classes via constraints, 206-220 [Zbl 0955.03020]  \\textit{Pichler, Reinhard}, Completeness and redundancy in constrained clause logic, 221-235 [Zbl 0955.03019]  \\textit{Pliu\u0161kevi\u010dien\u0117, Aida}, Effective properties of some first order intuitionistic modal logics, 236-250 [Zbl 0963.03034]  \\textit{Ro\u015fu, Grigore; Goguen, Joseph}, Hidden congruent deduction, 251-266 [Zbl 0964.68083]  \\textit{Sofronie-Stokkermans, Viorica}, Resolution-based theorem proving for \\(\\text{SH}_n\\)-logics, 267-281 [Zbl 0956.03009]  \\textit{Wirth, Claus-Peter}, Full first-order sequent and tableau calculi with preservation of solutions and the liberalized \\(\\delta\\)-rule but without Skolemization, 282-297 [Zbl 0955.03021]","type":"string"},"datatype":"string"},"type":"statement","id":"Q1967066$E787C6C9-72DC-4223-95AF-6C7C71CF3A62","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"342a6161f41187e2c595daa41b09cee10ab1ace9","datavalue":{"value":"00B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1967066$7AE47071-D73D-4EED-90D0-B6D1541F8B5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f1971b12f93143b2604d15a1750f495d71fae62d","datavalue":{"value":"03-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1967066$99586F3D-B898-42E1-B60A-D7BC3E06722C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1967066$0EA5F575-21A6-425A-8873-25F7C7D346D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1967066$E991F076-4C48-490E-A00D-193108AA0A7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1967066$D24F8CAA-8C62-49ED-98E4-5D6EE01D791C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bd67f45dc99e5f2e421af1edadd1add0b9a67e92","datavalue":{"value":"1412344","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1967066$689F8D18-BF02-4800-BB58-13CE2492208E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0bf4f74c129274c74f2df90abe98591d25c9e4a0","datavalue":{"value":"Automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1967066$58E813B2-2AC3-42A4-B2F0-60CC73C94A92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8b7ef681899129fcc10e93d2abdd1a5c3b674bbf","datavalue":{"value":"Classical logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1967066$152EE90C-9C92-4A29-A925-E4789C066165","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6e90b20176166bed6db14936b5eb0775748d18a","datavalue":{"value":"Non-classical logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1967066$6C60C8AF-4335-481F-B503-AAC0ABEB9EC8","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1967066$960F38FE-9B2E-4B38-9FEA-DC9E6C79D74B","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":"Q1967066$5C5991F8-0D6B-4D53-9ACF-EC1519BCDA4D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5e50c4e36c5e55a43c641ff80c3491a50eab2c99","datavalue":{"value":"https://doi.org/10.1007/3-540-46508-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q1967066$0B4B0109-B7DA-4E82-AB5F-14D13E7FCF6F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1ffc35e35a858e76fc5c25161b0c35da06e86e76","datavalue":{"value":"W2481077391","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1967066$26D0D495-4F36-474C-9EC7-2FD8B5B65266","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automated deduction in classical and non-classical logics. Selected papers","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Automated_deduction_in_classical_and_non-classical_logics._Selected_papers"}}}}}