scholarly journals Tree resolution proofs of the weak pigeon-hole principle

2002 ◽  
Author(s):  
S. Dantchev ◽  
S. Riis
Keyword(s):  
Pigeon Hole Principle ◽  
Resolution Proofs ◽  
Tree Resolution

scholarly journals A Complexity Gap for Tree-Resolution

1999 ◽  
Vol 6 (29) ◽  
Author(s):  
Søren Riis
Keyword(s):  
Predicate Logic ◽  
Proof Complexity ◽  
Polynomial Size ◽  
Combinatorial Principles ◽  
Resolution Proofs ◽  
Symmetrical Group ◽  
Tree Resolution ◽  
Single Proposition ◽  
Exponential Size ◽  
Recent Idea

<p>It is shown that any sequence  psi_n of tautologies which expresses the<br />validity of a fixed combinatorial principle either is "easy" i.e. has polynomial<br />size tree-resolution proofs or is "difficult" i.e requires exponential<br />size tree-resolution proofs. It is shown that the class of tautologies which<br />are hard (for tree-resolution) is identical to the class of tautologies which<br />are based on combinatorial principles which are violated for infinite sets.<br />Actually it is shown that the gap-phenomena is valid for tautologies based<br />on infinite mathematical theories (i.e. not just based on a single proposition).<br />We clarify the link between translating combinatorial principles (or<br />more general statements from predicate logic) and the recent idea of using<br /> the symmetrical group to generate problems of propositional logic.<br />Finally, we show that it is undecidable whether a sequence  psi_n (of the<br />kind we consider) has polynomial size tree-resolution proofs or requires<br />exponential size tree-resolution proofs. Also we show that the degree of<br />the polynomial in the polynomial size (in case it exists) is non-recursive,<br />but semi-decidable.</p><p>Keywords: Logical aspects of Complexity, Propositional proof complexity,<br />Resolution proofs.</p><p> </p>

scholarly journals Monophyly of Heterandriini (Teleostei: Poeciliidae) revisited: a critical review of the data

2012 ◽  
Vol 10 (1) ◽  
pp. 19-44 ◽  
Author(s):  
Alfy Morales-Cazan ◽  
James S. Albert
Keyword(s):  
Biological Sciences ◽  
Morphological Characters ◽  
Model Systems ◽  
Morphological Data ◽  
Maximum Parsimony Analysis ◽  
Fin Ray ◽  
Outgroup Species ◽  
Tree Topologies ◽  
Tree Resolution ◽  
Shape Morphometrics

The systematics and taxonomy of poeciliid fishes (guppies and allies) remain poorly understood despite the relative importance of these species as model systems in the biological sciences. This study focuses on testing the monophyly of the nominal poeciliine tribe Heterandriini and the genus Heterandria, through examination of the morphological characters on which the current classification is based. These characters include aspects of body shape (morphometrics), scale and fin-ray counts (meristics), pigmentation, the cephalic laterosensory system, and osteological features of the neurocranium, oral jaws and suspensorium, branchial basket, pectoral girdle, and the gonopodium and its supports. A Maximum Parsimony analysis was conducted of 150 characters coded for 56 poeciliid and outgroup species, including 22 of 45 heterandriin species (from the accounted in Parenti & Rauchenberger, 1989), or seven of nine heterandriin species (from the accounted in Lucinda & Reis, 2005). Multistate characters were analyzed as both unordered and ordered, and iterative a posteriori weighting was used to improve tree resolution. Tree topologies obtained from these analyses support the monophyly of the Middle American species of "Heterandria," which based on available phylogenetic information, are herein reassigned to the genus Pseudoxiphophorus. None of the characters used in previous studies to characterize the nominal taxon Heterandriini are found to be unambiguously diagnostic. Some of these characters are shared with species in other poeciliid tribes, and others are reversed within the Heterandriini. These results support the hypothesis that Pseudoxiphophorus is monophyletic, and that this clade is not the closest relative of H. formosa (the type species) from southeastern North America. Available morphological data are not sufficient to assess the phylogenetic relationships of H. formosa with respect to other members of the Heterandriini. The results further suggest that most tribe-level taxa of the Poeciliinae are not monophyletic, and that further work remains to resolve the evolutionary relationships of this group.

scholarly journals Proof Complexity of Modal Resolution

2021 ◽  
Author(s):  
Sarah Sigley ◽  
Olaf Beyersdorff
Keyword(s):  
Artificial Intelligence ◽  
Automated Reasoning ◽  
Proof Complexity ◽  
Pigeonhole Principle ◽  
Analytic Tableaux ◽  
Frege Systems ◽  
International Joint ◽  
Resolution Proofs ◽  
Exponential Size ◽  
Sixth International

AbstractWe investigate the proof complexity of modal resolution systems developed by Nalon and Dixon (J Algorithms 62(3–4):117–134, 2007) and Nalon et al. (in: Automated reasoning with analytic Tableaux and related methods—24th international conference, (TABLEAUX’15), pp 185–200, 2015), which form the basis of modal theorem proving (Nalon et al., in: Proceedings of the twenty-sixth international joint conference on artificial intelligence (IJCAI’17), pp 4919–4923, 2017). We complement these calculi by a new tighter variant and show that proofs can be efficiently translated between all these variants, meaning that the calculi are equivalent from a proof complexity perspective. We then develop the first lower bound technique for modal resolution using Prover–Delayer games, which can be used to establish “genuine” modal lower bounds for size of dag-like modal resolution proofs. We illustrate the technique by devising a new modal pigeonhole principle, which we demonstrate to require exponential-size proofs in modal resolution. Finally, we compare modal resolution to the modal Frege systems of Hrubeš (Ann Pure Appl Log 157(2–3):194–205, 2009) and obtain a “genuinely” modal separation.

A strange pigeon-hole principle

Order ◽  
1990 ◽  
Vol 7 (2) ◽  
pp. 107-113 ◽  
Author(s):  
J�nos Koml�s
Keyword(s):  
Pigeon Hole Principle

Lifting propositional proof compression algorithms to first-order logic

2020 ◽  
Author(s):  
Jan Gorzny ◽  
Ezequiel Postan ◽  
Bruno Woltzenlogel Paleo
Keyword(s):  
Propositional Logic ◽  
Empirical Evaluation ◽  
Order Logic ◽  
Automated Deduction ◽  
First Order Logic ◽  
Compression Algorithms ◽  
International Conference ◽  
First Order ◽  
Theorem Provers ◽  
Resolution Proofs

Abstract Proofs are a key feature of modern propositional and first-order theorem provers. Proofs generated by such tools serve as explanations for unsatisfiability of statements. However, these explanations are complicated by proofs which are not necessarily as concise as possible. There are a wide variety of compression techniques for propositional resolution proofs but fewer compression techniques for first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on lifting proof compression ideas used in propositional logic to first-order logic. The first approach lifted from propositional logic delays resolution with unit clauses, which are clauses that have a single literal. The second approach is partial regularization, which removes an inference $\eta $ when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference in every path from $\eta $ to the root of the proof. This paper describes the generalization of the algorithms LowerUnits and RecyclePivotsWithIntersection (Fontaine et al.. Compression of propositional resolution proofs via partial regularization. In Automated Deduction—CADE-23—23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31–August 5, 2011, p. 237--251. Springer, 2011) from propositional logic to first-order logic. The generalized algorithms compresses resolution proofs containing resolution and factoring inferences with unification. An empirical evaluation of these approaches is included.

Discriminating the effects of phylogenetic hypothesis, tree resolution and clade age estimates on phylogenetic signal measurements

Plant Biology ◽  
2012 ◽  
Vol 15 (5) ◽  
pp. 858-867 ◽  
Author(s):  
G. D. S. Seger ◽  
L. D. S. Duarte ◽  
V. J. Debastiani ◽  
A. Kindel ◽  
J. A. Jarenkow
Keyword(s):  
Phylogenetic Signal ◽  
Phylogenetic Hypothesis ◽  
Tree Resolution ◽  
Age Estimates
Sign in / Sign up

Export Citation Format

Share Document