{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,29]],"date-time":"2025-01-29T05:38:02Z","timestamp":1738129082179,"version":"3.33.0"},"reference-count":30,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2024,1,30]],"date-time":"2024-01-30T00:00:00Z","timestamp":1706572800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/pages\/standard-publication-reuse-rights"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,2,27]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Usually in logic, proof systems are defined having in mind proving properties like validity and semantic consequence. It seems worthwhile to address the problem of having proof systems where satisfiability is a primitive notion in the sense that a formal derivation means that a finite set of formulas is satisfiable. Moreover, it would be useful to cover within the same framework as many logics as possible. We consider Kripke semantics where the properties of the constructors are provided by valuation constraints as the common ground of those logics. This includes for instance intuitionistic logic, paraconsistent Nelson\u2019s logic ${\\textsf{N4}}$, paraconsistent logic ${\\textsf{imbC}}$ and modal logics among others. After specifying a logic by those valuation constraints, we show how to induce automatically and from scratch an existential proof system for that logic. The rules of the proof system are shown to be invertible. General results of soundness and completeness are proved and then applied to the logics at hand.<\/jats:p>","DOI":"10.1093\/jigpal\/jzad030","type":"journal-article","created":{"date-parts":[[2024,1,30]],"date-time":"2024-01-30T17:54:57Z","timestamp":1706637297000},"page":"173-201","source":"Crossref","is-referenced-by-count":0,"title":["Labelled proof systems for existential reasoning"],"prefix":"10.1093","volume":"33","author":[{"given":"Jaime","family":"Ramos","sequence":"first","affiliation":[{"name":"Departamento de Matem\u00e1tica, Instituto Superior T\u00e9cnico, ULisboa, Portugal , Instituto de Telecomunica\u00e7\u00f5es, Avenida Rovisco Pais, 1049-001 Lisboa, Portugal, jaime.ramos@tecnico.ulisboa.pt"}]},{"given":"Jo\u00e3o","family":"Rasga","sequence":"additional","affiliation":[{"name":"Departamento de Matem\u00e1tica, Instituto Superior T\u00e9cnico, ULisboa, Portugal , Instituto de Telecomunica\u00e7\u00f5es, Avenida Rovisco Pais, 1049-001 Lisboa, Portugal, joao.rasga@tecnico.ulisboa.pt"}]},{"given":"Cristina","family":"Sernadas","sequence":"additional","affiliation":[{"name":"Departamento de Matem\u00e1tica, Instituto Superior T\u00e9cnico, ULisboa, Portugal , Instituto de Telecomunica\u00e7\u00f5es, Avenida Rovisco Pais, 1049-001 Lisboa, Portugal, cristina.sernadas@tecnico.ulisboa.pt"}]}],"member":"286","published-online":{"date-parts":[[2024,1,30]]},"reference":[{"key":"2025012810511860200_ref1","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1023\/A:1014490210693","article-title":"A reasoning model based on the production of acceptable arguments","volume":"34","author":"Amgoud","year":"2002","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"2025012810511860200_ref2","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1305\/ndjfl\/1093636764","article-title":"Kripke-type semantics for da Costa\u2019s paraconsistent logic ${\\mathrm{C}}\\_{\\omega } $","volume":"27","author":"Baaz","year":"1986","journal-title":"Notre Dame Journal of Formal Logic"},{"volume-title":"Intuitionistic Logic","year":"2005","author":"Bezhanishvili","key":"2025012810511860200_ref3"},{"key":"2025012810511860200_ref4","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/978-3-030-06164-7_6","article-title":"Reasoning with ontologies","volume-title":"A Guided Tour of Artificial Intelligence Research: Volume I: Knowledge Representation, Reasoning and Learning","author":"Bienvenu","year":"2020"},{"key":"2025012810511860200_ref5","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"Blackburn","year":"2001"},{"key":"2025012810511860200_ref6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2814937","article-title":"Model checking existential logic on partially ordered sets","volume":"17","author":"Bova","year":"2015","journal-title":"ACM Transactions on Computational Logic"},{"key":"2025012810511860200_ref7","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1016\/j.tcs.2015.07.016","article-title":"Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics","volume":"603","author":"Caleiro","year":"2015","journal-title":"Theoretical Computer Science"},{"volume-title":"Paraconsistent Logic: Consistency, Contradiction and Negation","year":"2016","author":"Carnielli","key":"2025012810511860200_ref8"},{"key":"2025012810511860200_ref9","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4020-6324-4_1","article-title":"Logics of formal inconsistency","volume-title":"Handbook of Philosophical Logic","author":"Carnielli","year":"2007"},{"key":"2025012810511860200_ref10","first-page":"3790","article-title":"Calculs propositionnels pour les syst\u00e8mes formels inconsistants","volume":"257","author":"da Costa","year":"1963","journal-title":"Comptes Rendus Hebdomadaires des S\u00e9ances de l\u2019Acad\u00e9mie des Sciences"},{"key":"2025012810511860200_ref11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-94-017-0460-1_1","article-title":"Relevance logic","volume-title":"Handbook of Philosophical Logic","author":"Dunn","year":"2002"},{"key":"2025012810511860200_ref12","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/s10817-012-9252-7","article-title":"Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models","volume":"51","author":"Ferrari","year":"2013","journal-title":"Journal of Automated Reasoning"},{"key":"2025012810511860200_ref13","article-title":"Proof methods for modal and intuitionistic logics","author":"Fitting","year":"1983","journal-title":"Kluwer"},{"key":"2025012810511860200_ref14","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538332.001.0001","volume-title":"Labelled Deductive Systems","author":"Gabbay","year":"1996"},{"key":"2025012810511860200_ref15","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-981-15-2221-5_9","article-title":"Refutation systems: an overview and some applications to philosophical logics","volume-title":"Knowledge, Proof and Dynamics","author":"Goranko","year":"2020"},{"key":"2025012810511860200_ref16","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/978-3-540-40981-6_11","article-title":"Modeling adversaries in a logic for security protocol analysis","volume-title":"Formal Aspects of Security","author":"Halpern","year":"2003"},{"key":"2025012810511860200_ref17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.tcs.2011.11.001","article-title":"Proof theory of Nelson\u2019s paraconsistent logic: a uniform perspective","volume":"415","author":"Kamide","year":"2012","journal-title":"Theoretical Computer Science"},{"volume-title":"Proof Theory of N4 -Related Paraconsistent Logics","year":"2015","author":"Kamide","key":"2025012810511860200_ref18"},{"key":"2025012810511860200_ref19","doi-asserted-by":"crossref","first-page":"107","DOI":"10.18653\/v1\/2020.sigdial-1.14","article-title":"Learning and reasoning for robot dialog and navigation tasks","volume-title":"Proceedings of the 21th Annual Meeting of the Special Interest Group on Discourse and Dialogue","author":"Lu","year":"2020"},{"volume-title":"Aristotle\u2019s Syllogistic From the Standpoint of Modern Formal Logic","year":"1951","author":"\u0141ukasiewicz","key":"2025012810511860200_ref20"},{"key":"2025012810511860200_ref21","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/s11225-009-9196-z","article-title":"What is a non-truth-functional logic","volume":"92","author":"Marcos","year":"2009","journal-title":"Studia Logica"},{"key":"2025012810511860200_ref22","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/s10992-005-2267-3","article-title":"Proof analysis in modal logic","volume":"34","author":"Negri","year":"2005","journal-title":"Journal of Philosophical Logic"},{"key":"2025012810511860200_ref23","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/s11787-014-0097-1","article-title":"Proofs and countermodels in non-classical logics","volume":"8","author":"Negri","year":"2014","journal-title":"Logica Universalis"},{"key":"2025012810511860200_ref24","doi-asserted-by":"crossref","first-page":"16","DOI":"10.2307\/2268973","article-title":"Constructible falsity","volume":"14","author":"Nelson","year":"1949","journal-title":"The Journal of Symbolic Logic"},{"key":"2025012810511860200_ref25","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/3-540-45988-X_18","article-title":"Labelled deduction over algebras of truth-values","volume-title":"Frontiers of Combining Systems (Santa Margherita Ligure, 2002)","author":"Rasga","year":"2002"},{"volume-title":"Admissibility of Logical Inference Rules","year":"1997","author":"Rybakov","key":"2025012810511860200_ref26"},{"key":"2025012810511860200_ref27","doi-asserted-by":"crossref","first-page":"277","DOI":"10.3166\/jancl.13.277-315","article-title":"Truth-values as labels: a general recipe for labelled deduction","volume":"13","author":"Sernadas","year":"2003","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"2025012810511860200_ref28","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/s11787-009-0009-y","article-title":"A refutation theory","volume":"3","author":"Skura","year":"2009","journal-title":"Logica Universalis"},{"key":"2025012810511860200_ref29","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"Troelstra","year":"2000"},{"key":"2025012810511860200_ref30","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/j.jal.2017.01.002","article-title":"A more general general proof theory","volume":"25","author":"Wansing","year":"2017","journal-title":"Journal of Applied Logic"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/33\/1\/173\/56450434\/jzad030.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/33\/1\/173\/56450434\/jzad030.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,28]],"date-time":"2025-01-28T10:51:47Z","timestamp":1738061507000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/33\/1\/173\/7589908"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,30]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,2,27]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzad030","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"type":"print","value":"1367-0751"},{"type":"electronic","value":"1368-9894"}],"subject":[],"published-other":{"date-parts":[[2025,2]]},"published":{"date-parts":[[2024,1,30]]}}}