-
LEGO-like Small-Model Constructions for Åqvist's Logics
Authors:
Dmitry Rozplokhas
Abstract:
Å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 construct…
▽ More
Å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, obtained uniformly for 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.
△ Less
Submitted 28 April, 2024;
originally announced April 2024.
-
Streamlining Input/Output Logics with Sequent Calculi
Authors:
Agata Ciabattoni,
Dmitry Rozplokhas
Abstract:
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 logic…
▽ More
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.
△ Less
Submitted 15 June, 2023;
originally announced June 2023.
-
Scheduling Complexity of Interleaving Search
Authors:
Dmitry Rozplokhas,
Dmitry Boulytchev
Abstract:
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 reason…
▽ More
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.
△ Less
Submitted 4 March, 2022; v1 submitted 17 February, 2022;
originally announced February 2022.
-
The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them
Authors:
Ekaterina Komendantskaya,
Dmitry Rozplokhas,
Henning Basold
Abstract:
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 exten…
▽ More
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.
△ Less
Submitted 9 August, 2020;
originally announced August 2020.
-
Certified Semantics for Relational Programming
Authors:
Dmitry Rozplokhas,
Andrey Vyatkin,
Dmitry Boulytchev
Abstract:
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…
▽ More
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.
△ Less
Submitted 16 September, 2020; v1 submitted 3 May, 2020;
originally announced May 2020.
