| 1. |
- Adams, Robin, 1978, et al.
(författare)
-
Weyl's predicative classical mathematics as a logic-enriched type theory
- 2010
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1557-945X .- 1529-3785. ; 11:2
-
Tidskriftsartikel (refereegranskat)abstract
- We construct a logic-enriched type theory LTTW that corresponds closely to the predicative system of foundations presented by Hermann Weyl in Das Kontinuum. We formalize many results from that book in LTTW, including Weyl's definition of the cardinality of a set and several results from real analysis, using the proof assistant Plastic that implements the logical framework LF. This case study shows how type theory can be used to represent a nonconstructive foundation for mathematics.
|
|
| 2. |
- Albert, Elvira, et al.
(författare)
-
On the Inference of Resource Usage Upper and Lower Bounds
- 2013
-
Ingår i: ACM Transactions on Computational Logic. - : ACM Press. - 1529-3785 .- 1557-945X. ; 14:3, s. Article number 22-
-
Tidskriftsartikel (refereegranskat)abstract
- Cost analysis aims at determining the amount of resources required to run a program in terms of its input data sizes. The most challenging step is to infer the cost of executing the loops in the program. This requires bounding the number of iterations of each loop and finding tight bounds for the cost of each of its iterations. This article presents a novel approach to infer upper and lower bounds from cost relations. These relations are an extended form of standard recurrence equations that can be nondeterministic, contain inexact size constraints and have multiple arguments that increase and/or decrease. We propose novel techniques to automatically transform cost relations into worst-case and best-case deterministic one-argument recurrence relations. The solution of each recursive relation provides a preciseupper-bound and lower-bound for executing a corresponding loop in the program. Importantly, since the approach is developed at the level of the cost equations, our techniques are programming language independent.
|
|
| 3. |
- Atserias, Albert, et al.
(författare)
-
Narrow Proofs May Be Maximally Long
- 2016
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 17:3
-
Tidskriftsartikel (refereegranskat)abstract
- We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n(Omega(w)). This shows that the simple counting argument that any formula refutable in width w must have a proof in size n(O(w)) is essentially tight. Moreover, our lower bound generalizes to polynomial calculus resolution and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. The lower bound does not extend all the way to Lasserre, however, since we show that there the formulas we study have proofs of constant rank and size polynomial in both n and w.
|
|
| 4. |
- Beyersdorff, Olaf, et al.
(författare)
-
Parameterized Complexity of DPLL Search Procedures
- 2013
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 14:3, s. 20-
-
Tidskriftsartikel (refereegranskat)abstract
- We study the performance of DPLL algorithms on parameterized problems. In particular, we investigate how difficult it is to decide whether small solutions exist for satisfiability and other combinatorial problems. For this purpose we develop a Prover-Delayer game that models the running time of DPLL procedures and we establish an information-theoretic method to obtain lower bounds to the running time of parameterized DPLL procedures. We illustrate this technique by showing lower bounds to the parameterized pigeonhole principle and to the ordering principle. As our main application we study the DPLL procedure for the problem of deciding whether a graph has a small clique. We show that proving the absence of a k-clique requires n(Omega(k)) steps for a nontrivial distribution of graphs close to the critical threshold. For the restricted case of tree-like Parameterized Resolution, this result answers a question asked by Beyersdorff et al. [2012] of understanding the Resolution complexity of this family of formulas.
|
|
| 5. |
- Bodirsky, Manuel, et al.
(författare)
-
The Complexity of Phylogeny Constraint Satisfaction Problems
- 2017
-
Ingår i: ACM Transactions on Computational Logic. - : ASSOC COMPUTING MACHINERY. - 1529-3785 .- 1557-945X. ; 18:3
-
Tidskriftsartikel (refereegranskat)abstract
- We systematically study the computational complexity of a broad class of computational problems in phylogenetic reconstruction. The class contains, for example, the rooted triple consistency problem, forbidden subtree problems, the quartet consistency problem, and many other problems studied in the bioinformatics literature. The studied problems can be described as constraint satisfaction problems, where the constraints have a first-order definition over the rooted triple relation. We show that every such phylogeny problem can be solved in polynomial time or is NP-complete. On the algorithmic side, we generalize a well-known polynomial-time algorithm of Aho, Sagiv, Szymanski, and Ullman for the rooted triple consistency problem. Our algorithm repeatedly solves linear equation systems to construct a solution in polynomial time. We then show that every phylogeny problem that cannot be solved by our algorithm is NP-complete. Our classification establishes a dichotomy for a large class of infinite structures that we believe is of independent interest in universal algebra, model theory, and topology. The proof of our main result combines results and techniques from various research areas: a recent classification of the model-complete cores of the reducts of the homogeneous binary branching C-relation, Leebs Ramsey theorem for rooted trees, and universal algebra.
|
|
| 6. |
- Cerrito, Serenella, et al.
(författare)
-
Optimal Tableaux Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-time Temoral Logic ATL
- 2015
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 17:1
-
Tidskriftsartikel (refereegranskat)abstract
- We develop a sound, complete, and practically implementable tableau-based decision method for constructive satisfiability testing and model synthesis for the fragment ATL+ of the full alternating-time temporal logic ALT*. The method extends in an essential way a previously developed tableau-based decision method for ATL and works in 2EXPTIME, which is the optimal worst-case complexity of the satisfiability problem for ATL+. We also discuss how suitable parameterizations and syntactic restrictions on the class of input ATL+formulas can reduce the complexity of the satisfiability problem.
|
|
| 7. |
- Creignou, Nadia, et al.
(författare)
-
Complexity Classifications for Logic-Based Argumentation
- 2014
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 15:3, s. 19-
-
Tidskriftsartikel (refereegranskat)abstract
- We consider logic-based argumentation in which an argument is a pair (Phi, alpha), where the support Phi is a minimal consistent set of formulae taken from a given knowledge base (usually denoted by Delta) that entails the claim alpha (a formula). We study the complexity of three central problems in argumentation: the existence of a support Phi subset of Delta, the verification of a support, and the relevance problem (given psi, is there a support Phi such that psi is an element of Phi?). When arguments are given in the frill language of propositional logic, these problems are computationally costly tasks: the verification problem is DP-complete; the others are Sigma(P)(2)-complete. We study these problems in Schaefers famous framework where the considered propositional formulae are in generalized conjunctive normal form. This means that formulae are conjunctions of constraints built upon a fixed finite set of Boolean relations Gamma (the constraint language). We show that according to the properties of this language Gamma, deciding whether there exists a support for a claim in a given knowledge base is either polynomial, NP-complete, coNP-complete, or Sigma(P)(2)-complete. We present a dichotomous classification, P or DP-complete, for the verification problem and a trichotomous classification for the relevance problem into either polynomial, NP-complete, or Sigma(P)(2)-complete. These last two classifications are obtained by means of algebraic tools.
|
|
| 8. |
- Drabent, Włodzimierz
(författare)
-
Correctness and Completeness of Logic Programs
- 2016
-
Ingår i: ACM Transactions on Computational Logic. - : ACM Special Interest Group on Computer Science Education. - 1529-3785 .- 1557-945X. ; 17:3
-
Tidskriftsartikel (refereegranskat)abstract
- We discuss proving correctness and completeness of definite clause logic programs. We propose a method for proving completeness, while for proving correctness we employ a method which should be well known but is often neglected. Also, we show how to prove completeness and correctness in the presence of SLD-tree pruning, and point out that approximate specifications simplify specifications and proofs.We compare the proof methods to declarative diagnosis (algorithmic debugging), showing that approximate specifications eliminate a major drawback of the latter. We argue that our proof methods reflect natural declarative thinking about programs, and that they can be used, formally or informally, in every-day programming.
|
|
| 9. |
- Enqvist, Sebastian, et al.
(författare)
-
The Temporal Logic of Coalitional Goal Assignments in Concurrent Multiplayer Games
- 2022
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 23:4
-
Tidskriftsartikel (refereegranskat)abstract
- We introduce and study a natural extension of the Alternating time temporal logic ATL, called Temporal Logic of Coalitional Goal Assignments (TLCGA). It features one new and quite expressive coalitional strategic operator, called the coalitional goal assignment operator ⦉ γ ⦊, where γ is a mapping assigning to each set of players in the game its coalitional goal, formalised by a path formula of the language of TLCGA, i.e., a formula prefixed with a temporal operator X, U, or G, representing a temporalised objective for the respective coalition, describing the property of the plays on which that objective is satisfied. Then, the formula ⦉ γ ⦊ intuitively says that there is a strategy profile Σ for the grand coalition Agt such that for each coalition C, the restriction Σ |C of Σ to C is a collective strategy of C that enforces the satisfaction of its objective γ (C) in all outcome plays enabled by Σ |C.We establish fixpoint characterizations of the temporal goal assignments in a μ-calculus extension of TLCGA, discuss its expressiveness and illustrate it with some examples, prove bisimulation invariance and Hennessy–Milner property for it with respect to a suitably defined notion of bisimulation, construct a sound and complete axiomatic system for TLCGA, and obtain its decidability via finite model property.
|
|
| 10. |
- Fichte, Johannes Klaus, 1983-, et al.
(författare)
-
Strong Backdoors for Default Logic
- 2024
-
Ingår i: ACM Transactions on Computational Logic. - : ACM Digital Library. - 1529-3785 .- 1557-945X.
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper, we introduce a notion of backdoors to Reiter’s propositional default logic and study structural properties of it. Also we consider the problems of backdoor detection (parameterised by the solution size) as well as backdoor evaluation (parameterised by the size of the given backdoor), for various kinds of target classes (CNF, KROM, MONOTONE) and all SCHAEFER classes. Also, we study generalisations of HORN-formulas, namely, QHORN, RHORN, as well as DUALHORN. For these classes, we also classify the computational complexity of the implication problem. We show that backdoor detection is fixed-parameter tractable for the considered target classes, and prove a complete trichotomy for backdoor evaluation. The problems are either fixed-parameter tractable, para-DeltaP2-complete, or para-NP-complete, depending on the target class.
|
|
| 11. |
- Filmus, Y., et al.
(författare)
-
From small space to small width in resolution
- 2015
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 16:4
-
Tidskriftsartikel (refereegranskat)abstract
- In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of a Conjunctive Normal Form (CNF) formula is always an upper bound on the width needed to refute the formula. Their proof is beautiful but uses a nonconstructive argument based on Ehrenfeucht-Fraïssé games. We give an alternative, more explicit, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexitymeasure that works against any resolution refutation-previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similarmethods.
|
|
| 12. |
- Goranko, Valentin, et al.
(författare)
-
Game-Theoretic Semantics for Alternating-Time Temporal Logic
- 2018
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 19:3
-
Tidskriftsartikel (refereegranskat)abstract
- We introduce several versions of game-theoretic semantics (GTS) for Alternating-Time Temporal Logic (ATL). In GTS, truth is defined in terms of existence of a winning strategy in a semantic evaluation game. Thus, the game-theoretic perspective appears in the framework of ATL on two semantic levels: on the object level in the standard semantics of the strategic operators and on the meta-level, where game-theoretic logical semantics is applied to ATL. We unify these two perspectives into semantic evaluation games specially designed for ATL. The game-theoretic perspective enables us to identify new variants of the semantics of ATL based on limiting the time resources available to the verifier and falsifier in the semantic evaluation game. We introduce and analyze an unbounded and (ordinal) bounded GTS and prove these to be equivalent to the standard (Tarski-style) compositional semantics. We show that, in bounded GTS, truth of ATL formulae can always be determined in finite time, that is, without constructing infinite paths. We also introduce a nonequivalent finitely bounded semantics and argue that it is natural from both logical and game-theoretic perspectives.
|
|
| 13. |
- Gratzer, Daniel, et al.
(författare)
-
Modalities and Parametric Adjoints
- 2022
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 23:3
-
Tidskriftsartikel (refereegranskat)abstract
- Birkedal et al. recently introduced dependent right adjoints as an important class of (non-fibered) modalities in type theory. We observe that several aspects of their calculus are left underdeveloped and that it cannot serve as an internal language. We resolve these problems by assuming that the modal context operator is a parametric right adjoint. We show that this hitherto unrecognized structure is common. Based on these discoveries we present a new well-behaved Fitch-style multimodal type theory, which can be used as an internal language. Finally, we apply this syntax to guarded recursion and parametricity.
|
|
| 14. |
- Heras, Jónathan, et al.
(författare)
-
Computing persistent homology within Coq/SSReflect
- 2013
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 14:4
-
Tidskriftsartikel (refereegranskat)abstract
- Persistent homology is one of the most active branches of Computational Algebraic Topology with applications in several contexts such as optical character recognition or analysis of point cloud data. In this paper, we report on the formal development of certified programs to compute persistent Betti numbers, an instrumental tool of persistent homology, using the Coq proof assistant together with the SSReflect extension. To this aim it has been necessary to formalize the underlying mathematical theory of these algorithms. This is another example showing that interactive theorem provers have reached a point where they are mature enough to tackle the formalization of nontrivial mathematical theories.
|
|
| 15. |
- Kraus, H., et al.
(författare)
-
Higher homotopies in a hierarchy of univalent universes
- 2015
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1557-945X .- 1529-3785. ; 16:2, s. 18:1-18:12
-
Tidskriftsartikel (refereegranskat)abstract
- For Martin-Löf type theory with a hierarchy U_0 : U_1 : U_2 : … of univalent universes, we show that U_n is not an n-type. Our construction also solves the problem of finding a type that strictly has some high truncation level without using higher inductive types. In particular, U_n is such a type if we restrict it to n-types. We have fully formalized and verified our results within the dependently typed language and proof assistant Agda.
|
|
| 16. |
- Mahmood, Y., et al.
(författare)
-
Parameterized Complexity of Logic-based Argumentation in Schaefer's Framework
- 2023
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 24:3
-
Tidskriftsartikel (refereegranskat)abstract
- Argumentation is a well-established formalism dealing with conflicting information by generating and comparing arguments. It has been playing a major role in AI for decades. In logic-based argumentation, we explore the internal structure of an argument. Informally, a set of formulas is the support for a given claim if it is consistent, subset-minimal, and implies the claim. In such a case, the pair of the support and the claim together is called an argument. In this article, we study the propositional variants of the following three computational tasks studied in argumentation: ARG (exists a support for a given claim with respect to a given set of formulas), ARG-Check (is a given set a support for a given claim), and ARG-Rel (similarly as ARG plus requiring an additionally given formula to be contained in the support). ARG-Check is complete for the complexity class DP, and the other two problems are known to be complete for the second level of the polynomial hierarchy (Creignou et al. 2014 and Parson et al., 2003) and, accordingly, are highly intractable. Analyzing the reason for this intractability, we perform a two-dimensional classification: First, we consider all possible propositional fragments of the problem within Schaefer's framework (STOC 1978) and then study different parameterizations for each of the fragments. We identify a list of reasonable structural parameters (size of the claim, support, knowledge base) that are connected to the aforementioned decision problems. Eventually, we thoroughly draw a fine border of parameterized intractability for each of the problems showing where the problems are fixed-parameter tractable and when this exactly stops. Surprisingly, several cases are of very high intractability (para-NP and beyond).
|
|
| 17. |
- Nordström, Jakob
(författare)
-
On the Relative Strength of Pebbling and Resolution
- 2012
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 13:2, s. 16-
-
Tidskriftsartikel (refereegranskat)abstract
- The last decade has seen a revival of interest in pebble games in the context of proof complexity. Pebbling has proven to be a useful tool for studying resolution-based proof systems when comparing the strength of different subsystems, showing bounds on proof space, and establishing size-space trade-offs. The typical approach has been to encode the pebble game played on a graph as a CNF formula and then argue that proofs of this formula must inherit (various aspects of) the pebbling properties of the underlying graph. Unfortunately, the reductions used here are not tight. To simulate resolution proofs by pebblings, the full strength of nondeterministic black-white pebbling is needed, whereas resolution is only known to be able to simulate deterministic black pebbling. To obtain strong results, one therefore needs to find specific graph families which either have essentially the same properties for black and black-white pebbling (not at all true in general) or which admit simulations of black-white pebblings in resolution. This article contributes to both these approaches. First, we design a restricted form of black-white pebbling that can be simulated in resolution and show that there are graph families for which such restricted pebblings can be asymptotically better than black pebblings. This proves that, perhaps somewhat unexpectedly, resolution can strictly beat black-only pebbling, and in particular that the space lower bounds on pebbling formulas in Ben-Sasson and Nordstr " om [2008] are tight. Second, we present a versatile parametrized graph family with essentially the same properties for black and black-white pebbling, which gives sharp simultaneous trade-offs for black and black-white pebbling for various parameter settings. Both of our contributions have been instrumental in obtaining the time-space trade-off results for resolution-based proof systems in Ben-Sasson and Nordstr " om [2011].
|
|
| 18. |
- Oetsch, Johannes, et al.
(författare)
-
Beyond Uniform Equivalence between Answer-set Programs
- 2021
-
Ingår i: ACM Transactions on Computational Logic. - : ACM Digital Library. - 1529-3785 .- 1557-945X. ; 22:1
-
Tidskriftsartikel (refereegranskat)abstract
- This article deals with advanced notions of equivalence between nonmonotonic logic programs under the answer-set semantics, a topic of considerable interest, because such notions form the basis for program verification and are useful for program optimisation, debugging, and modular programming. In fact, there is extensive research in answer-set programming (ASP) dealing with different notions of equivalence between programs. Prominent among these notions is uniform equivalence, which checks whether two programs have the same semantics when joined with an arbitrary set of facts. In this article, we study a family of more fine-grained versions of uniform equivalence, viz. relativised uniform equivalence with projection, which extends standard uniform equivalence in terms of two additional parameters: One for specifying the input alphabet and one for specifying the output alphabet for programs. In particular, the second parameter is used for projecting answer sets to a set of designated output atoms. Answer-set projection, in particular, allows to compare programs that make use of different auxiliary atoms, which is important for practical programming aspects. We introduce novel semantic characterisations for the program correspondence problems under consideration and analyse their computational complexity. In the general case, deciding these problems lies on the third level of the polynomial hierarchy. Therefore, this task cannot be efficiently reduced to propositional answer-set programs itself (under the usual complexity-theoretic assumptions). However, reductions to quantified Boolean formulas (QBFs) are feasible. Indeed, we provide efficient (in fact, linear-time constructible) reductions to QBFs and discuss simplifications for certain special cases. These QBF reductions yield the basis for a prototype implementation, the system cc ĝŠCurrency sign, for deciding correspondence problems by using off-the-shelf QBF solvers. We discuss an application of cc ĝŠCurrency sign for verifying the correctness of solutions by students drawn from a laboratory course on logic programming and knowledge representation at the Technische Universität Wien, employing relativised uniform equivalence with projection as the underlying program correspondence notion.
|
|
