Publications
2025
- JELIAGL-based Calculi for PCL and its Deontic CousinAgata Ciabattoni, Dmitry Rozplokhas, and Matteo Tesi19th European Conf. on Logics in Artificial Intelligence, Kutaisi, Georgia, 2025
We introduce a natural sequent calculus for preferential conditional logic PCL via embeddings into provability logic GL, achieving optimal complexity and enabling countermodel extraction. Extending the method to PCL with reflexivity and absoluteness – corresponding to Åqvist’s deontic system F with cautious monotony – we employ hypersequents to capture the S5 modality; the resulting calculus subsumes the known calculi for the weaker systems E and F within Åqvist family.
- IJCAIA Non-Interventionist Approach to Causal Reasoning based on Lewisian CounterfactualsCarlos Aguilera-Ventura, Xinghan Liu, Emiliano Lorini, and Dmitry Rozplokhas34th Int. Joint Conf. on Artificial Intelligence, Montreal, Canada, 2025
We present a computationally grounded semantics for counterfactual conditionals in which i) the state in a model is decomposed into two elements: a propositional valuation and a causal base in propositional form that represents the causal information available at the state; and ii) the comparative similarity relation between states is computed from the states’ two components. We show that, by means of our semantics, we can elegantly formalize the notion of actual cause without recurring to the primitive notion of intervention. Furthermore, we provide a succinct formulation of the model checking problem for a language of counterfactual conditionals in our semantics. We show that this problem is PSPACE-complete and provide a reduction of it into QBF that can be used for automatic verification of causal properties.
- TARKGraded Distributed BeliefEmiliano Lorini, and Dmitry Rozplokhas21st Conf. on Theoretical Aspects of Rationality and Knowledge, Düsseldorf, Germany, 2025
We introduce a new logic of graded distributed belief that allows us to express the fact that a coalition of agents distributively believes that a certain fact \varphi holds with at least strength k. We interpret our logic by means of computationally grounded semantics relying on the concept of belief base. The strength of the coalition’s distributed belief is directly computed from the coalition’s belief base after having merged its members’ individual belief bases. We illustrate our logic with some intuitive examples and provide a sound and complete Hilbert-style axiomatization as well as a decidability result obtained via filtration. Last but not least, we present a decision procedure for our logic based on tableaux that allows us to state PSPACE-completeness for our logic.
2024
- KRStrongly Analytic Calculi for KLM Logics with SMT-Based ProverAgata Ciabattoni, Clemens Eisenhofer, and Dmitry Rozplokhas21st Int. Conf. on Principles of Knowledge Representation and Reasoning, Hanoi, Vietnam, 2024
We introduce modular calculi for the logics for nonmonotonic reasoning defined by Kraus, Lehmann, and Magidor, featuring a strengthened form of analyticity. Our calculi are used to determine the computational complexity for the logics C, CL, CM, P (and M), and fragments thereof. The calculi are encoded into SMT solvers, yielding an efficient prover with countermodel generation capabilities. Our work encompasses known results and introduces new findings, including co-NP-completeness and a more effective semantics for C.
@inproceedings{StronglyAnalyticKLM, author = {Ciabattoni, Agata and Eisenhofer, Clemens and Rozplokhas, Dmitry}, editor = {Marquis, Pierre and Ortiz, Magdalena and Pagnucco, Maurice}, title = {Strongly Analytic Calculi for {KLM} Logics with SMT-Based Prover}, booktitle = {Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, {KR} 2024, Hanoi, Vietnam. November 2-8, 2024}, year = {2024}, url = {https://doi.org/10.24963/kr.2024/27}, doi = {10.24963/KR.2024/27}, } - AiMLLEGO-Like Small Model Constructions for Åqvist’s LogicsDmitry Rozplokhas15th Int. Conf. on Advances in Modal Logic, Prague, Czech Republic, 2024
Åqvist’s logics (E, F, F+(CM), and G) are among the best-known systems in the long tradition of preference-based approaches for modeling conditional obligation. While the general semantics of preference models align well with philosophical intuitions, more constructive characterizations are needed to assess computational complexity and facilitate automated deduction. Existing small model constructions from conditional logics (due to Friedman and Halpern) are applicable only to F+(CM) and G, while recently developed proof-theoretic characterizations leave unresolved the exact complexity of theoremhood in logic F. In this paper, we introduce alternative small model constructions assembled from elementary building blocks, applicable uniformly to all four Åqvist’s logics. Our constructions propose alternative semantical characterizations and imply co-NP-completeness of theoremhood. Furthermore, they can be naturally encoded in classical propositional logic for automated deduction.
@inproceedings{LEGOModels, author = {Rozplokhas, Dmitry}, editor = {Ciabattoni, Agata and Gabelaia, David and Sedl{\'{a}}r, Igor}, title = {LEGO-Like Small Model Constructions for {\AA}qvist's Logics}, booktitle = {Advances in Modal Logic, AiML 2024, Prague, Czech Republic, August 19-23, 2024}, pages = {631--652}, publisher = {College Publications}, year = {2024}, }
2023
- KRStreamlining Input/Output Logics with Sequent CalculiAgata Ciabattoni, and Dmitry Rozplokhas20th Int. Conf. on Principles of Knowledge Representation and Reasoning, Rhodes, Greece, 2023Ray Reiter Best Paper Prize
Input/Output (I/O) logic is a general framework for reasoning about conditional norms and/or causal relations. We streamline Bochman’s causal I/O logics via proof-search-oriented sequent calculi. Our calculi establish a natural syntactic link between the derivability in these logics and in the original I/O logics. As a consequence of our results, we obtain new, simple semantics for all these logics, complexity bounds, embeddings into normal modal logics, and efficient deduction methods. Our work encompasses many scattered results and provides uniform solutions to various unresolved problems.
@inproceedings{StreamliningIO, author = {Ciabattoni, Agata and Rozplokhas, Dmitry}, editor = {Marquis, Pierre and Son, Tran Cao and Kern{-}Isberner, Gabriele}, title = {Streamlining Input/Output Logics with Sequent Calculi}, booktitle = {Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, {KR} 2023, Rhodes, Greece, September 2-8, 2023}, pages = {146--155}, year = {2023}, url = {https://doi.org/10.24963/kr.2023/15}, doi = {10.24963/kr.2023/15}, } - DEONAnalytic Proof Theory for Åqvist’s System F16th Int. Conf. on Deontic Logic and Normative Systems, Trois-Rivières, Canada, 2023
The key strength of preference-based logics for conditional obligation is their ability to handle contrary-to-duty paradoxes and account for exceptions. Here we investigate Åqvist’s system F, a well-known logic in this family. F has the notable feature that every satisfiable formula has a “best” element. Thus far, the only proof system for F was a Hilbert calculus, impeding applications and deeper investigations. We fill this gap, constructing the first analytic calculus for F. The calculus possesses good proof-theoretical properties—in particular, cut-elimination, which greatly facilitates proof search. Our calculus is used to provide explanations of logical consequences, as a decision-making tool, and to obtain a preliminary complexity upper bound for F (giving a theoretical limit on its automated behavior).
@inproceedings{AnalyticF, author = {Ciabattoni, Agata and Olivetti, Nicola and Parent, Xavier and Ramanayake, Revantha and Rozplokhas, Dmitry}, editor = {Maranh{\~{a}}o, Juliano and Peterson, Clayton and Stra{\ss}er, Christian and van der Torre, Leendert}, title = {Analytic Proof Theory for {\AA}qvist's System {F}}, booktitle = {Proceedings of the 16th International Conference on Deontic Logic and Normative Systems, {DEON} 2023, Trois-Rivi{\`{e}}res, QC, Canada, July 5-7, 2023}, pages = {79--98}, publisher = {College Publications}, year = {2023}, }
2022
- FLOPSScheduling Complexity of Interleaving SearchDmitry Rozplokhas, and Dmitry Boulytchev16th Int. Symp. on Functional and Logic Programming, online, 2022
miniKanren is a lightweight embedded language for logic and relational programming. Many of its useful features come from a distinctive search strategy, called interleaving search. However, with interleaving search conventional ways of reasoning about the complexity and performance of logical programs become irrelevant. We identify an important key component – scheduling – which makes the reasoning for miniKanren so different, and present a semi-automatic technique to estimate the scheduling impact via symbolic execution for a reasonably wide class of programs.
@inproceedings{InterleavingSchedulingComplexity, author = {Rozplokhas, Dmitry and Boulytchev, Dmitry}, editor = {Hanus, Michael and Igarashi, Atsushi}, title = {Scheduling Complexity of Interleaving Search}, booktitle = {Proceedings of the 16th International Symposium on Functional and Logic Programming, {FLOPS} 2022, Kyoto, Japan, May 10-12, 2022}, series = {Lecture Notes in Computer Science}, volume = {13215}, pages = {152--170}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-030-99461-7\_9}, doi = {10.1007/978-3-030-99461-7\_9}, }
2020
- ICLPThe New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore ThemEkaterina Komendantskaya, Dmitry Rozplokhas, and Henning Basold36th Int. Conf. on Logic Programming, online, 2020
In sequent calculi, cut elimination is a property that guarantees that any provable formula can be proven analytically. For example, Gentzen’s classical and intuitionistic calculi LK and LJ enjoy cut elimination. The property is less studied in coinductive extensions of sequent calculi. In this paper, we use coinductive Horn clause theories to show that cut is not eliminable in a coinductive extension of LJ, a system we call CLJ. We derive two further practical results from this study. We show that CoLP by Gupta et al. gives rise to cut-free proofs in CLJ with fixpoint terms, and we formulate and implement a novel method of coinductive theory exploration that provides several heuristics for discovery of cut formulae in CLJ.
@inproceedings{CoinductiveCuts, author = {Komendantskaya, Ekaterina and Rozplokhas, Dmitry and Basold, Henning}, title = {The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them}, booktitle = {Theory Pract. Log. Program, 36th International Conference on Logic Programming Special Issue II}, pages = {990--1005}, publisher = {Cambridge University Press}, year = {2020}, url = {https://doi.org/10.1017/S1471068420000423}, doi = {10.1017/S1471068420000423}, } - APLASCertified Semantics for Relational ProgrammingDmitry Rozplokhas, Andrey Vyatkin, and Dmitry Boulytchev18th Asian Symp. on Programming Languages and Systems, online, 2020
We present a formal study of semantics for the relational programming language miniKanren. First, we formulate a denotational semantics which corresponds to the minimal Herbrand model for definite logic programs. Second, we present operational semantics which models interleaving, the distinctive feature of miniKanren implementation, and prove its soundness and completeness w.r.t. the denotational semantics. Our development is supported by a Coq specification, from which a reference interpreter can be extracted. We also derive from our main result a certified semantics (and a reference interpreter) for SLD resolution with cut and prove its soundness.
@inproceedings{miniKanrenCertifiedSemantics, author = {Rozplokhas, Dmitry and Vyatkin, Andrey and Boulytchev, Dmitry}, editor = {d. S. Oliveira, Bruno C.}, title = {Certified Semantics for Relational Programming}, booktitle = {Proceedings of the 18th Asian Symposium on Programming Languages and Systems, {APLAS} 2020, Fukuoka, Japan, November 30 - December 2, 2020}, series = {Lecture Notes in Computer Science}, volume = {12470}, pages = {167--185}, publisher = {Springer}, year = {2020}, url = {https://doi.org/10.1007/978-3-030-64437-6\_9}, doi = {10.1007/978-3-030-64437-6\_9}, }
2018
- PPDPImproving Refutational Completeness of Relational Search via Divergence TestDmitry Rozplokhas, and Dmitry Boulytchev20th Int. Symp. on Principles and Practice of Declarative Programming, Frankfurt am Main, Germany, 2018
We describe a search optimization technique for implementation of relational programming language miniKanren which makes more queries converge. Specifically, we address the problem of conjunction non-commutativity. Our technique is based on a certain divergence criterion that we use to trigger a dynamic reordering of conjuncts. We present a formal semantics of a miniKanren-like language and prove that our optimization does not compromise already converging programs, thus, being a proper improvement. We also present the prototype implementation of the improved search and demonstrate its application for a number of realistic specifications.
@inproceedings{ImprovingRefutationalCompleteness, author = {Rozplokhas, Dmitry and Boulytchev, Dmitry}, editor = {Sabel, David and Thiemann, Peter}, title = {Improving Refutational Completeness of Relational Search via Divergence Test}, booktitle = {Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, {PPDP} 2018, Frankfurt am Main, Germany, September 03-05, 2018}, pages = {18:1--18:13}, publisher = {{ACM}}, year = {2018}, url = {https://doi.org/10.1145/3236950.3236958}, doi = {10.1145/3236950.3236958}, }