Logic in Computer Science
New submissions
[ showing up to 1000 entries per page: fewer | more ]
New submissions for Wed, 24 Apr 24
- [1] arXiv:2404.14470 [pdf, ps, other]
-
Title: Truth FactorsAuthors: Robert E. KentComments: 38 pages, 18 figuresSubjects: Logic in Computer Science (cs.LO)
Truth refers to the satisfaction relation used to define the semantics of model-theoretic languages. The satisfaction relation for first order languages (truth classification), and the preservation of truth by first order interpretations (truth infomorphism), is a motivating example in the theory of Information Flow (IF) (Barwise and Seligman 1997). The abstract theory of satisfaction is the basis for the theory of institutions (Goguen and Burstall 1992). Factoring refers to categorical factorization systems. The concept lattice, which is the central structure studied by the theory of Formal Concept Analysis (FCA) (Ganter and Wille 1999), is constructed by a factorization. The study of classification structures (IF) and the study of conceptual structures (FCA) aim (at least is part) to provide a principled foundation for the logical theory of knowledge representation and organization. In an effort to unify these two areas, the paper "Distributed Conceptual Structures" (Kent 2002) abstracted the basic theorem of FCA in order to established three levels of categorical equivalence between classification structures and conceptual structures. In this paper we refine this approach by resolving the equivalence as the factorization of three isomorphic versions: relation, function and Galois connection. We develop the latter more algebraic version of the equivalence as the polar factorization of Galois connections. We advocate this abstract adjunctive representation of classification and conceptual structures.
- [2] arXiv:2404.14517 [pdf, ps, other]
-
Title: Synthesis for prefix first-order logic on data wordsSubjects: Logic in Computer Science (cs.LO)
We study the reactive synthesis problem for distributed systems with an unbounded number of participants interacting with an uncontrollable environment. Executions of those systems are modeled by data words, and specifications are given as first-order logic formulas from a fragment we call prefix first-order logic that implements a limited kind of order. We show that this logic has nice properties that enable us to prove decidability of the synthesis problem.
- [3] arXiv:2404.14781 [pdf, other]
-
Title: Improved Algorithm for Reachability in $d$-VASSComments: 36 pagesSubjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL)
An $\mathsf{F}_{d}$ upper bound for the reachability problem in vector addition systems with states (VASS) in fixed dimension is given, where $\mathsf{F}_d$ is the $d$-th level of the Grzegorczyk hierarchy of complexity classes. The new algorithm combines the idea of the linear path scheme characterization of the reachability in the $2$-dimension VASSes with the general decomposition algorithm by Mayr, Kosaraju and Lambert. The result improves the $\mathsf{F}_{d + 4}$ upper bound due to Leroux and Schmitz (LICS 2019).
- [4] arXiv:2404.14919 [pdf, other]
-
Title: Stalnaker's Epistemic Logic in Isabelle/HOLAuthors: Laura P. Gamboa Guzman (Iowa State University, Ames, Iowa), Kristin Y. Rozier (Iowa State University, Ames, Iowa)Comments: In Proceedings LSFA/HCVS 2023, arXiv:2404.13672Journal-ref: EPTCS 402, 2024, pp. 4-17Subjects: Logic in Computer Science (cs.LO)
The foundations of formal models for epistemic and doxastic logics often rely on certain logical aspects of modal logics such as S4 and S4.2 and their semantics; however, the corresponding mathematical results are often stated in papers or books without including a detailed proof, or a reference to it, that allows the reader to convince themselves about them. We reinforce the foundations of the epistemic logic S4.2 for countably many agents by formalizing its soundness and completeness results for the class of all weakly-directed pre-orders in the proof assistant Isabelle/HOL. This logic corresponds to the knowledge fragment, i.e., the logic for formulas that may only include knowledge modalities in Stalnaker's system for knowledge and belief. Additionally, we formalize the equivalence between two axiomatizations for S4, which are used depending on the type of semantics given to the modal operators, as one is commonly used for the relational semantics, and the other one arises naturally from the topological semantics.
- [5] arXiv:2404.14920 [pdf, other]
-
Title: Formalizing Factorization on Euclidean Domains and Abstract Euclidean AlgorithmsAuthors: Thaynara Arielly de Lima (Universidade Federal de Goiás), Andréia Borges Avelar (Universidade de Brasília), André Luiz Galdino (Universidade Federal de Catalão), Mauricio Ayala-Rincón (Universidade de Brasília)Comments: In Proceedings LSFA/HCVS 2023, arXiv:2404.13672Journal-ref: EPTCS 402, 2024, pp. 18-33Subjects: Logic in Computer Science (cs.LO)
This paper discusses the extension of the Prototype Verification System (PVS) sub-theory for rings, part of the PVS algebra theory, with theorems related to the division algorithm for Euclidean rings and Unique Factorization Domains that are general structures where an analog of the Fundamental Theorem of Arithmetic holds. First, we formalize the general abstract notions of divisibility, prime, and irreducible elements in commutative rings, essential to deal with unique factorization domains. Then, we formalize the landmark theorem, establishing that every principal ideal domain is a unique factorization domain. Finally, we specify the theory of Euclidean domains and formally verify that the rings of integers, the Gaussian integers, and arbitrary fields are Euclidean domains. To highlight the benefits of such a general abstract discipline of formalization, we specify a Euclidean gcd algorithm for Euclidean domains and formalize its correctness. Also, we show how this correctness is inherited under adequate parameterizations for the structures of integers and Gaussian integers.
- [6] arXiv:2404.14921 [pdf, ps, other]
-
Title: More Church-Rosser Proofs in BELUGAAuthors: Alberto Momigliano (Dipartimento di Informatica, Università degli Studi di Milano, Italy), Martina Sassella (Dipartimento di Matematica, Università degli Studi di Milano, Italy)Comments: In Proceedings LSFA/HCVS 2023, arXiv:2404.13672Journal-ref: EPTCS 402, 2024, pp. 34-42Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
We report on yet another formalization of the Church-Rosser property in lambda-calculi, carried out with the proof environment Beluga. After the well-known proofs of confluence for beta-reduction in the untyped settings, with and without Takahashi's complete developments method, we concentrate on eta-reduction and obtain the result for beta-eta modularly. We further extend the analysis to typed-calculi, in particular System F. Finally, we investigate the idea of pursuing the encoding directly in Beluga's meta-logic, as well as the use of Beluga's logic programming engine to search for counterexamples.
- [7] arXiv:2404.14922 [pdf, ps, other]
-
Title: Semi-Substructural Logics with AdditivesAuthors: Niccolò Veltri (Tallinn University of Technology), Cheng-Syuan Wan (Tallinn University of Technology)Comments: In Proceedings LSFA/HCVS 2023, arXiv:2404.13672Journal-ref: EPTCS 402, 2024, pp. 63-80Subjects: Logic in Computer Science (cs.LO)
This work concerns the proof theory of (left) skew monoidal categories and their variants (e.g. closed monoidal, symmetric monoidal), continuing the line of work initiated in recent years by Uustalu et al. Skew monoidal categories are a weak version of Mac Lane's monoidal categories, where the structural laws are not required to be invertible, they are merely natural transformations with a specific orientation. Sequent calculi which can be modelled in such categories can be identified as deductive systems for restricted substructural fragments of intuitionistic linear logic. These calculi enjoy cut elimination and admit a focusing strategy, sharing resemblance with Andreoli's normalization technique for linear logic. The focusing procedure is useful for solving the coherence problem of the considered categories with skew structure.
Here we investigate possible extensions of the sequent calculi of Uustalu et al. with additive connectives. As a first step, we extend the sequent calculus with additive conjunction and disjunction, corresponding to studying the proof theory of skew monoidal categories with binary products and coproducts satisfying a left-distributivity condition. We introduce a new focused sequent calculus of derivations in normal form, which employs tag annotations to reduce non-deterministic choices in bottom-up proof search. The focused sequent calculus and the proof of its correctness have been formalized in the Agda proof assistant. We also discuss extensions of the logic with additive units, a form of skew exchange and linear implication. - [8] arXiv:2404.14923 [pdf, ps, other]
-
Title: CHC-COMP 2023: Competition ReportAuthors: Emanuele De Angelis (IASI-CNR, Rome, Italy), Hari Govind V K (University of Waterloo, Canada)Comments: In Proceedings LSFA/HCVS 2023, arXiv:2404.13672Journal-ref: EPTCS 402, 2024, pp. 83-104Subjects: Logic in Computer Science (cs.LO)
CHC-COMP 2023 is the sixth edition of the Competition of Solvers for Constrained Horn Clauses. The competition was run in April 2023 and the results were presented at the 10th Workshop on Horn Clauses for Verification and Synthesis held in Paris, France, on April 23, 2023. This edition featured seven solvers (six competing and one hors concours) and six tracks, each of which dealing with a class of clauses. This report describes the organization of CHC-COMP 2023 and presents its results.
- [9] arXiv:2404.14924 [pdf, other]
-
Title: An Encoding for CLP Problems in SMT-LIBComments: In Proceedings LSFA/HCVS 2023, arXiv:2404.13672Journal-ref: EPTCS 402, 2024, pp. 118-130Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
The input language for today's CHC solvers are commonly the standard SMT-LIB format, borrowed from SMT solvers, and the Prolog format that stems from Constraint-Logic Programming (CLP). This paper presents a new front-end of the Eldarica CHC solver that allows inputs in the Prolog language. We give a formal translation of a subset of Prolog into the SMT-LIB commands. Our initial experiments show the effectiveness of the approach and the potential benefits to both the CHC solving and CLP communities.
- [10] arXiv:2404.15214 [pdf, other]
-
Title: Embedding Differential Dynamic Logic in PVSAuthors: J. Tanner Slagel (NASA), Mariano Moscato (NIA), Lauren White (NASA), César A. Muñoz (NASA), Swee Balachandran (NIA), Aaron Dutle (NASA)Comments: In Proceedings LSFA/HCVS 2023, arXiv:2404.13672Journal-ref: EPTCS 402, 2024, pp. 43-62Subjects: Logic in Computer Science (cs.LO)
Differential dynamic logic (dL) is a formal framework for specifying and reasoning about hybrid systems, i.e., dynamical systems that exhibit both continuous and discrete behaviors. These kinds of systems arise in many safety- and mission-critical applications. This paper presents a formalization of dL in the Prototype Verification System (PVS) that includes the semantics of hybrid programs and dL's proof calculus. The formalization embeds dL into the PVS logic, resulting in a version of dL whose proof calculus is not only formally verified, but is also available for the verification of hybrid programs within PVS itself. This embedding, called Plaidypvs (Properly Assured Implementation of dL for Hybrid Program Verification and Specification), supports standard dL style proofs, but further leverages the capabilities of PVS to allow reasoning about entire classes of hybrid programs. The embedding also allows the user to import the well-established definitions and mathematical theories available in PVS.
- [11] arXiv:2404.15215 [pdf, other]
-
Title: Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software VerificationAuthors: Márk Somorjai (Department of Measurement and Information Systems, Budapest University of Technology and Economics), Mihály Dobos-Kovács (Department of Measurement and Information Systems, Budapest University of Technology and Economics), Zsófia Ádám (Department of Measurement and Information Systems, Budapest University of Technology and Economics), Levente Bajczi (Department of Measurement and Information Systems, Budapest University of Technology and Economics), András Vörös (Department of Measurement and Information Systems, Budapest University of Technology and Economics)Comments: In Proceedings LSFA/HCVS 2023, arXiv:2404.13672. This research was partially funded by the UNKP-22-2,3-I New National Excellence Program and Project no. 2019-1.3.1-KK-2019-00004, which has been implemented with the support provided from the National Research, Development and Innovation Fund of Hungary, financed under the 2019-1.3.1-KK funding schemeJournal-ref: EPTCS 402, 2024, pp. 105-117Subjects: Logic in Computer Science (cs.LO); Software Engineering (cs.SE)
Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique.
- [12] arXiv:2404.15221 [pdf, ps, other]
-
Title: The Architecture of TruthAuthors: Robert E. KentComments: 62 pages, 6 figuresSubjects: Logic in Computer Science (cs.LO)
The theory of institutions is framed as an indexed/fibered duality, where the indexed aspect specifies the fibered aspect. Tarski represented truth in terms of a satisfaction relation. The theory of institutions encodes satisfaction as its core architecture in the indexed aspect. Logical environments enrich this truth architecture by axiomatizing the truth adjunction in the fibered aspect. The truth architecture is preserved by morphisms of logical environments. (Although not every institution is a logical environment, each institution has an associated logical environment defined via the intent of the structures of the institution, and each institution is represented by an indexed functor into the structure category of the classification logical environment $\mathtt{Cls}$.)
- [13] arXiv:2404.15248 [pdf, ps, other]
-
Title: A Dependency Pair Framework for Relative Termination of Term RewritingSubjects: Logic in Computer Science (cs.LO)
Dependency pairs are one of the most powerful techniques for proving termination of term rewrite systems (TRSs), and they are used in almost all tools for termination analysis of TRSs. Problem #106 of the RTA List of Open Problems asks for an adaption of dependency pairs for relative termination. Here, infinite rewrite sequences are allowed, but one wants to prove that a certain subset of the rewrite rules cannot be used infinitely often. Dependency pairs were recently adapted to annotated dependency pairs (ADPs) to prove almost-sure termination of probabilistic TRSs. In this paper, we develop a novel adaption of ADPs for relative termination. We implemented our new ADP framework in our tool AProVE and evaluate it in comparison to state-of-the-art tools for relative termination of TRSs.
Cross-lists for Wed, 24 Apr 24
- [14] arXiv:2404.14789 (cross-list from cs.MA) [pdf, other]
-
Title: Opinion Update in a Subjective Logic Model for Social NetworksSubjects: Multiagent Systems (cs.MA); Logic in Computer Science (cs.LO)
Subjective Logic (SL) is a logic incorporating uncertainty and opinions for agents in dynamic systems. In this work, we investigate the use of subjective logic to model opinions and belief change in social networks. In particular, we work toward the development of a subjective logic belief/opinion update function appropriate for modeling belief change as communication occurs in social networks. We found through experiments that an update function with belief fusion from SL does not have ideal properties to represent a rational update. Even without these properties, we found that an update function with cumulative belief fusion can describe behaviors not explored by the social network model defined by Alvim, Knight, and Valencia (2019).
Replacements for Wed, 24 Apr 24
- [15] arXiv:2401.11752 (replaced) [pdf, other]
-
Title: Univalent Enriched Categories and the Enriched Rezk CompletionAuthors: Niels van der WeideSubjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)
- [16] arXiv:2402.13552 (replaced) [pdf, ps, other]
-
Title: Confluence of Logically Constrained Rewrite Systems RevisitedComments: Accepted at the 12th International Joint Conference on Automated Reasoning 2024Subjects: Logic in Computer Science (cs.LO)
[ showing up to 1000 entries per page: fewer | more ]
Disable MathJax (What is MathJax?)
Links to: arXiv, form interface, find, cs, recent, 2404, contact, help (Access key information)