{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T08:07:50Z","timestamp":1750666070781},"reference-count":31,"publisher":"Oxford University Press (OUP)","issue":"2","license":[{"start":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T00:00:00Z","timestamp":1643155200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,2,26]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present hypersequent calculi for the strongest logics in Lewis\u2019 family of conditional systems, characterized by uniformity and total reflexivity. We first present a non-standard hypersequent calculus, which allows a syntactic proof of cut elimination. We then introduce standard hypersequent calculi, in which sequents are enriched by additional structures to encode plausibility formulas and diamond formulas. Proof search using these calculi is terminating, and the completeness proof shows how a countermodel can be constructed from a branch of a failed proof search. We then describe tuCLEVER, a theorem prover that implements the standard hypersequent calculi. The prover provides a decision procedure for the logics, and it produces a countermodel in case of proof search failure. The prover tuCLEVER is inspired by the methodology of leanTAP and it is implemented in Prolog. Preliminary experimental results show that the performances of tuCLEVER are promising.1<\/jats:p>","DOI":"10.1093\/logcom\/exab084","type":"journal-article","created":{"date-parts":[[2021,12,18]],"date-time":"2021-12-18T12:09:28Z","timestamp":1639829368000},"page":"233-280","source":"Crossref","is-referenced-by-count":3,"title":["Calculi, countermodel generation and theorem prover for strong logics of counterfactual reasoning"],"prefix":"10.1093","volume":"32","author":[{"given":"Marianna","family":"Girlando","sequence":"first","affiliation":[{"name":"University of Birmingham, Birmingham, B15 2TT, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bj\u00f6rn","family":"Lellmann","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Wien, Vienna, A-1040, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicola","family":"Olivetti","sequence":"additional","affiliation":[{"name":"Aix Marseille Universit\u00e9, CNRS, ENSAM, Universit\u00e9 de Toulon, LSIS UMR 7296, 13397, Marseille, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Pesce","sequence":"additional","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e0 di Torino, Torino, 10149, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gian Luca","family":"Pozzato","sequence":"additional","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e0 di Torino, Torino, 10149, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2022,1,26]]},"reference":[{"key":"2022022805591832000_ref1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2010.04.002","article-title":"Csl-lean: a theorem-prover for the logic of comparative concept similarity","volume":"262","author":"Alenda","year":"2010","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2022022805591832000_ref2","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538622.003.0001","article-title":"The method of hypersequents in the proof theory of propositional non-classical logics","volume-title":"Logic: From Foundations to Applications","author":"Avron","year":"1996"},{"key":"2022022805591832000_ref3","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/BF00881804","article-title":"leantap: lean tableau-based deduction","volume":"15","author":"Beckert","year":"1995","journal-title":"Journal of Automated Reasoning"},{"key":"2022022805591832000_ref4","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1305\/ndjfl\/1093883341","article-title":"Quick completeness proofs for some logics of conditionals","volume":"22","author":"Burgess","year":"1981","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"2022022805591832000_ref5","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/BF00693270","article-title":"Basic conditional logic","volume":"4","author":"Chellas","year":"1975","journal-title":"Journal of Philosophical Logic"},{"key":"2022022805591832000_ref6","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1016\/B978-1-4832-1452-8.50115-9","article-title":"On the complexity of conditional logics","volume-title":"Principles of Knowledge Representation and Reasoning","author":"Friedman","year":"1994"},{"key":"2022022805591832000_ref7","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/1507244.1507251","article-title":"Tableau calculus for preference-based conditional logics","volume":"10","author":"Giordano","year":"2009","journal-title":"ACM Transactions on Computational Logic"},{"key":"2022022805591832000_ref8","first-page":"199","article-title":"Theorem proving for lewis logics of counterfactual reasoning","volume-title":"Proceedings of the 35th Italian Conference on Computational Logic\u2014CILC 2020, Rende, Italy, October 13\u201315, 2020. CEUR Workshop Proceedings","author":"Girlando","year":"2020"},{"key":"2022022805591832000_ref9","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/978-3-319-48758-8_18","article-title":"Standard sequent calculi for Lewis\u2019 logics of counterfactuals","volume-title":"Logics in Artificial Intelligence","author":"Girlando","year":"2016"},{"key":"2022022805591832000_ref10","first-page":"131","article-title":"Hypersequent calculi for Lewis\u2019 conditional logics with uniformity and reflexivit","volume-title":"Automated Reasoning With Analytic Tableaux and Related Methods\u201426th International Conference, TABLEAUX 2017, Bras\u00edlia, Brazil, September 25\u201328, 2017","author":"Girlando","year":"2017"},{"key":"2022022805591832000_ref11","first-page":"149","article-title":"VINTE: an implementation of internal calculi for lewis\u2019 logics of counterfactual reasoning","volume-title":"Automated Reasoning With Analytic Tableaux and Related Methods\u201426th International Conference, TABLEAUX 2017, Bras\u00edlia, Brazil, September 25\u201328, 2017, Proceedings","author":"Girlando","year":"2017"},{"key":"2022022805591832000_ref12","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1093\/logcom\/8.1.87","article-title":"Updates and counterfactuals","volume":"8","author":"Grahne","year":"1998","journal-title":"Journal of Logic and Computation"},{"key":"2022022805591832000_ref13","volume-title":"An Introduction to Modal Logic","author":"Hughes","year":"1968"},{"key":"2022022805591832000_ref14","first-page":"387","article-title":"On the difference between updating a knowledge base and revising it","volume-title":"Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR\u201991). Cambridge, MA, USA, April 22\u201325, 1991","author":"Katsuno","year":"1991"},{"key":"2022022805591832000_ref15","volume-title":"Introduction to Metamathematics","author":"Kleene","year":"1952"},{"key":"2022022805591832000_ref16","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/0004-3702(90)90101-5","article-title":"Nonmonotonic reasoning, preferential models and cumulative logics","volume":"44","author":"Kraus","year":"1990","journal-title":"Artificial Intelligence"},{"key":"2022022805591832000_ref17","volume-title":"Sequent Calculi With Context Restrictions and Applications to Conditional Logic","author":"Lellmann","year":"2013"},{"key":"2022022805591832000_ref18","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1016\/j.tcs.2016.10.004","article-title":"Hypersequent rules with restricted contexts for propositional modal logics","volume":"656","author":"Lellmann","year":"2016","journal-title":"Theoretical Computer Science"},{"key":"2022022805591832000_ref19","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1007\/978-3-642-33353-8_25","article-title":"Sequent systems for Lewis\u2019 conditional logics","volume-title":"Logics in Artificial Intelligence","author":"Lellmann","year":"2012"},{"key":"2022022805591832000_ref20","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/978-3-642-40537-2_19","article-title":"Correspondence between modal hilbert axioms and sequent rules with an application to S5","volume-title":"Automated Reasoning With Analytic Tableaux and Related Methods","author":"Lellmann","year":"2013"},{"key":"2022022805591832000_ref21","volume-title":"Counterfactuals","author":"Lewis","year":"1973"},{"key":"2022022805591832000_ref22","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-009-8966-5","volume-title":"Topics in Conditional Logic","author":"Nute","year":"1980"},{"key":"2022022805591832000_ref23","doi-asserted-by":"crossref","first-page":"427","DOI":"10.3166\/jancl.18.427-473","article-title":"Theorem proving for conditional logics: CondLean and GoalDuck","volume":"18","author":"Olivetti","year":"2008","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"2022022805591832000_ref24","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/11554554_27","article-title":"Condlean 3.0: improving condlean for stronger conditional logics","volume-title":"Automated Reasoning With Analytic Tableaux and Related Methods: 14th International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005. Proceedings","author":"Olivetti","year":"2005"},{"key":"2022022805591832000_ref25","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1007\/978-3-319-08587-6_39","article-title":"NESCOND: an implementation of nested sequent calculi for conditional logics","volume-title":"Automated Reasoning","author":"Olivetti","year":"2014"},{"key":"2022022805591832000_ref26","doi-asserted-by":"crossref","first-page":"109","DOI":"10.3233\/IA-150082","article-title":"Nested sequent calculi and theorem proving for normal conditional logics: the theorem prover NESCOND","volume":"9","author":"Olivetti","year":"2015","journal-title":"Intelligenza Artificiale"},{"key":"2022022805591832000_ref27","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1007\/978-3-319-24312-2_19","article-title":"A standard internal calculus for lewis\u2019 counterfactual logics","volume-title":"Automated Reasoning With Analytic Tableaux and Related Methods","author":"Olivetti","year":"2015"},{"key":"2022022805591832000_ref28","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1017\/CBO9780511546464.012","article-title":"Proofnets for S5: sequents and circuits for modal logic","volume-title":"Logic Colloquium 2005","author":"Restall","year":"2007"},{"key":"2022022805591832000_ref29","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1093\/logcom\/exm007","article-title":"A logic for concepts and similarity","volume":"17","author":"Sheremet","year":"2007","journal-title":"Journal of Logic and Computation"},{"key":"2022022805591832000_ref30","first-page":"98","article-title":"A theory of conditionals","volume-title":"Studies in Logical Theory","author":"Stalnaker","year":"1968"},{"key":"2022022805591832000_ref31","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2273315","article-title":"A Gentzen- or Beth-type system, a practical decision procedure and a constructive completeness proof for the counterfactual logics $\\mathbb {V}\\mathbb {C}$ and $\\mathbb {V}\\mathbb {C}\\mathbb {S}$","volume":"48","author":"de Swart","year":"1983","journal-title":"The Journal of Symbolic Logic"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/32\/2\/233\/42618184\/exab084.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/32\/2\/233\/42618184\/exab084.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,14]],"date-time":"2023-11-14T12:57:51Z","timestamp":1699966671000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/32\/2\/233\/6513774"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,26]]},"references-count":31,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2022,1,26]]},"published-print":{"date-parts":[[2022,2,26]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exab084","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2022,3]]},"published":{"date-parts":[[2022,1,26]]}}}