| 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.
|
|
