This paper investigates the depth of resolution proofs, that is to say, the length of the longest path in the proof from an input clause to the conclusion. An abstract characterization of the measure is given, as well as a discussion of its relation to other measures of space complexity for resolution proofs.

The length of resolution proofs is investigated, relative to the model-theoretic measure of Herband complexity. A concept of resolution deduction is introduced which is somewhat more general than the classical concepts. It is shown that proof complexity is exponential in terms of Herband complexity and that this bound is tight. The concept of R-deduction is extended to FR-deduction, where, besides resolution, a function introduction rule is allowed. As an example, consider the clause P Q: conclude P) (...) Q, where a, f are new function symbols extending Herbrand's universe. P ()Q from Q) and Skolemization). By modification of a construction of Statman it is shown that FR-deductions may be nonelementarily shorter than R-deductions. Finally it is proved that FR-deduction has weaker effects only if clausal logic is restricted to Horn logic. (shrink)

In the 1920s, Paul Hertz (1881-1940) developed certain calculi based on structural rules only and established normal form results for proofs. It is shown that he anticipated important techniques and results of general proof theory as well as of resolution theory, if the latter is regarded as a part of structural proof theory. Furthermore, it is shown that Gentzen, in his first paper of 1933, which heavily draws on Hertz, proves a normal form result which corresponds to (...) the completeness of prepositional SLD-resolution in logic programming. (shrink)

We develop and study the complexity of propositional proof systems of varying strength extending resolution by allowing it to operate with disjunctions of linear equations instead of clauses. We demonstrate polynomial-size refutations for hard tautologies like the pigeonhole principle, Tseitin graph tautologies and the clique-coloring tautologies in these proof systems. Using interpolation we establish an exponential-size lower bound on refutations in a certain, considerably strong, fragment of resolution over linear equations, as well as a general polynomial (...) upper bound on interpolants in this fragment.We then apply these results to extend and improve previous results on multilinear proofs , as studied in [Ran Raz, Iddo Tzameret, The strength of multilinear proofs. Comput. Complexity ]. Specifically, we show the following:• Proofs operating with depth-3 multilinear formulas polynomially simulate a certain, considerably strong, fragment of resolution over linear equations.• Proofs operating with depth-3 multilinear formulas admit polynomial-size refutations of the pigeonhole principle and Tseitin graph tautologies. The former improve over a previous result that established small multilinear proofs only for the functional pigeonhole principle. The latter are different from previous proofs, and apply to multilinear proofs of Tseitin mod p graph tautologies over any field of characteristic 0. We conclude by connecting resolution over linear equations with extensions of the cutting planes proof system. (shrink)

A pool resolution proof is a dag-like resolution proof which admits a depth-first traversal tree in which no variable is used as a resolution variable twice on any branch. The problem of determining whether a given dag-like resolution proof is a valid pool resolution proof is shown to be NP-complete.

We prove constructively that for any propositional formula in Conjunctive Normal Form, we can either find a satisfying assignment of true and false to its variables, or a refutation of showing that it is unsatisfiable. This refutation is a resolution proof of ¬. From the formalization of our proof in Coq, we extract Robinson’s famous resolution algorithm as a Haskell program correct by construction. The account is an example of the genre of highly readable formalized mathematics.

We prove an exponential lower bound on the length of cutting plane proofs. The proof uses an extension of a lower bound for monotone circuits to circuits which compute with real numbers and use nondecreasing functions as gates. The latter result is of independent interest, since, in particular, it implies an exponential lower bound for some arithmetic circuits.

Resolution and cut-free LK are the most popular propositional systems used for logical automated reasoning. The question whether or not resolution and cut-free LK have the same efficiency on the system of CNF formulas has been asked and studied since 1960 425–467). It was shown in Cook and Reckhow, J. Symbolic Logic 44 36–50 that tree resolution has super-polynomial speed-up over cut-free LK. Naturally, the current issue is whether or not resolution and cut-free LK expressed as (...) directed acyclic graphs have the same efficiency. In this paper, we introduce a new algorithm to eliminate atomic cuts and show that cut-free LK polynomially simulates resolution when the input formula is expressed as a k-CNF formula. As a corollary, we show that regular resolution does not polynomially simulate cut-free LK. We also show that cut-free LK polynomially simulates regular resolution. (shrink)

This chapter shows the resolution of six difficulties for a mathematicist account of judicial proof. It first reports the difficulty about conjunction. It also addresses the difficulty about inference. The non-complementational negation principle for inductive probability ensures that, on an inductivist account, the standard of proof in civil cases does not officially condone a positive probability of injustice. Proof beyond reasonable doubt is proof at the level of inductive certainty. The inductivist analysis elucidates why ordinary (...) juries are competent to assess judicial proofs. Moreover, convergence and corroboration, and their appropriate independence conditions, can be readily explained in terms of inductive probability, with no difficulty arising about prior probabilities. (shrink)

"We present a proof-theoretic foundation for logic programming in Girard's linear logic. We exploit the permutability properties of two-sided linear sequent calculus to identify appropriate notions of uniform proof, definite formula, goal formula, clause and resolution proof for fragments of linear logic. The analysis of this paper extends earlier work by the present authors to include negative occurrences of [cross] (par) and positive occurences of! (of course!) and? (why not?). These connectives introduce considerable difficulty. We consider (...) briefly some of the issues related to the mechanical implementation of our resolution proofs.". (shrink)

This paper presents a formulation and completeness proof of the resolution-type calculi for the first order fragment of Girard's linear logic by a general method which provides the general scheme of transforming a cutfree Gentzen-type system into a resolution type system, preserving the structure of derivations. This is a direct extension of the method introduced by Maslov for classical predicate logic. Ideas of the author and Zamov are used to avoid skolomization. Completeness of strategies is first established (...) for the Gentzen-type system, and then transferred to resolution. The propositional resolution system was implemented by T. Tammet. (shrink)

Resolutions of choice spaces capture hierarchical processes of choice. Cantone, Giar-lotta and Watson (2021) formalize the concept in the setting of deterministic choice. We extend the notion of a resolution to probabilistic choices. Our main result is about the random utility model, also known as the multiple choice model (MCM, characterized by Falmagne in 1978). It states that any resolution of probabilistic choices satisfying the MCM also satisfies the MCM. We provide three proofs, each offering specific insights. In (...) contrast, Luce model (1959) of probabilistic choice is not preserved by resolutions. A probabilistic choice is hierarchical if it is equal to the outcome of some nontrivial resolution. Our second result is a simpler characterization of such choices, as those admitting a shrinkable subset. Here a shrinkable subset is a collection of elements that are, intuitively, indistinguishable from outside the collection. Our final result establishes that special ‘single-point’ resolutions suffice to generate all resolutions. (shrink)

Resolution is an effective deduction procedure for classical logic. There is no similar "resolution" system for non-classical logics (though there are various automated deduction systems). The paper presents resolution systems for intuistionistic predicate logic as well as for modal and temporal logics within the framework of labelled deductive systems. Whereas in classical predicate logic resolution is applied to literals, in our system resolution is applied to L(abelled) R(epresentation) S(tructures). Proofs are discovered by a refutation procedure (...) defined on LRSs, that imposes a hierarchy on clause sets of such structures together with an inheritance discipline. This is a form of Theory Resolution. For intuitionistic logic these structures are called I(ntuitionistic) R(epresentation) S(tructures). Their hierarchical structure allows the restriction of unification of individual variables and/or constants without using Skolem functions. This structures must therefore be preserved when we consider other (non-modal) logics. Variations between different logics are captured by fine tuning of the inheritance properties of the hierarchy. For modal and temporal logics IRS's are extended to structures that represent worlds and/or times. This enables us to consider all kinds of combined logics. (shrink)

We establish a connection between the geometric methods developed in the combinatorial theory of small cancellation and the propositional resolution calculus. We define a precise correspondence between resolution proofs in logic and diagrams in small cancellation theory, and as a consequence, we derive that a resolution proof is a 2-dimensional process. The isoperimetric function defined on diagrams corresponds to the length of resolution proofs.

We examine in some detail a series of papers published by P. Del Pezzo and C. Segre on the resolution of singularities of algebraic surfaces, trying to point out the main ideas. In 1888 P. Del Pezzo published a proof of the resolution of singularities of algebraic surfaces using birational transformations. He introduced the notion of “equisingularity” of two surfaces at a point or along a curve. This notion is made specific in a paper of 1889. C. (...) Segre in his famous paper on “infinitely near multiple points” on a surface published in 1896 shows that Del Pezzo's method does not always produce a smooth surface. During 1897 each author reasserts his point of view in several papers which contain interesting remarks, regardless of their increasingly polemic style. (shrink)

Most automated theorem provers have been built around some version of resolution [4]. But resolution is an inherently Classical logic technique. Attempts to extend the method to other logics have tended to obscure its simplicity. In this paper we present a resolution style theorem prover for Intuitionistic logic that, we believe, retains many of the attractive features of Classical resolution. It is, of course, more complicated, but the complications can be given intuitive motivation. We note that (...) a small change in the system as presented here causes it to collapse back to a Classical resolution system. We present the system in some detail for the propositional case, including soundness and completeness proofs. For the first order version we are sketchier. (shrink)

ABSTRACT This paper introduces a multi-valued variant of higher-order resolution and proves it correct and complete with respect to a variant of Henkin's general model semantics. This resolution method is parametric in the number of truth values as well as in the particular choice of the set of connectives (given by arbitrary truth tables) and even substitutional quantifiers. In the course of the completeness proof we establish a model existence theorem for this logical system. The work reported (...) in this paper provides a basis for developing higher-order mechanizations for many non-classical logics. (shrink)

The proof theory of many-valued systems has not been investigated to an extent comparable to the work done on axiomatizatbility of many-valued logics. Proof theory requires appropriate formalisms, such as sequent calculus, natural deduction, and tableaux for classical (and intuitionistic) logic. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory of (...) finite-valued first order logics in a general way, and to present some of the more important results in this area. In Systems covered are the resolution calculus, sequent calculus, tableaux, and natural deduction. This report is actually a template, from which all results can be specialized to particular logics. (shrink)

In advanced books and courses on logic (e.g. Sm], BM]) Gentzen-type systems or their dual, tableaux, are described as techniques for showing validity of formulae which are more practical than the usual Hilbert-type formalisms. People who have learnt these methods often wonder why the Automated Reasoning community seems to ignore them and prefers instead the resolution method. Some of the classical books on AD (such as CL], Lo]) do not mention these methods at all. Others (such as Ro]) do, (...) but the connections and reasons for preference remain unclear after reading them (at least to the present author, and obviously also the authors of OS], in which a theorem-prover, based exclusively on tableaux, is described). The confusion becomes greater when the reader is introduced to Kowalski's form of a clause ( Ko], Bu]), which is nothing but a Gentzen's sequent of atomic formulae, and when he realizes that resolution is just a form of a Cut, and so that while the elimination of cuts is the principal tool in proof-theory, its use is the main technique in AD! (shrink)

A necessary refinement of the concept of circular reasoning is applied to the self-and-universally-referential inductive justification of induction. It is noted that the assumption necessary for the circular proof of a principle of induction is that one inference is valid, not that the entire principle or rule of induction governing that inference is true. The circularity in an ideal case is demonstrated to have a value of lin where n represents the number of inferences asserted valid by the conclusion (...) of the justifying argument, and the ‘I’ represents the inference necessarily assumed valid.An induction antinomy modeled after Russell’s antinomy of the set of all and only non-self-containing sets is derived. Isomorphic antinomies are noted to be derivable for other arguments of philosophical interest, including those purported to undermine theories of determinism, relativism, and skepticism, and including the one that Descartes reduced and converted to ‘Cogito, ergo sum’. (shrink)

The study aims to show that the Kantian distinction of synthetic and analytical resolution of the courts is originally epistemic and not purely logical. Proof of this proposition is done so that in the first step are distinguished two types of synthetic and analytical predicate relation to the subject - logical-semantic and epistemic. Furthermore, the examples demonstrated that Kant was familiar cases in courts, which are found only logico-semantic synthetic or analytic connection of concepts in trials. Consequently, Kant (...) care for them and are therefore not in terms classifiable Critique of Pure Reason, Kant even offers a way to understand its logic and Prolegomena. Based on various Kant notes offered by Article resolution three types of synthetic courts and courts of two kinds of analysis. The final part of the article is devoted to a brief outline of the relationship of epistemic and epistemic-synthetic-analytic courts, because the courts are due to which Kant its resolution synthetic and analytical courts instituted . Shown is both preferred synthesis of ideas before analysis, first, how Kant based his teachings on unum, verum, bonum featured specific tasks analysis concepts. article is supplemented by a short reflection on Kant's definition of the principle of the dispute and by showing a significant difference between Kant and Bolzano definition of analytic courts, whose oversight can lead to misunderstanding the context in which resolution synthetic and analytical courts in Kant belongs. (shrink)

Scientific anomalies are observations and facts that contradict current scientific theories and they are instrumental in scientific theory change. Philosophers of science have approached scientific theory change from different perspectives as Darden (Theory change in science: Strategies from Mendelian genetics, 1991) observes: Lakatos (In: Lakatos, Musgrave (eds) Criticism and the growth of knowledge, 1970) approaches it as a progressive “research programmes” consisting of incremental improvements (“monster barring” in Lakatos, Proofs and refutations: The logic of mathematical discovery, 1976), Kuhn (The structure (...) of scientific revolutions, 1996) observes that changes in “paradigms” are instigated by a crisis from some anomaly, and Hanson (In: Feigl, Maxwell (eds) Current issues in the philosophy of science, 1961) proposes that discovery does not begin with hypothesis but with some “problematic phenomena requiring explanation”. Even though anomalies are important in all of these approaches to scientific theory change, there have been only few investigations into the specific role anomalies play in scientific theory change. Furthermore, much of these approaches focus on the theories themselves and not on how the scientists and their experiments bring about scientific change (Gooding, Experiment and the making of meaning: Human agency in scientific observation and experiment, 1990). To address these issues, this paper approaches scientific anomaly resolution from a meaning construction point of view. Conceptual integration theory (Fauconnier and Turner, Cogn Sci 22:133–187, 1996; The way we think: Conceptual blending and mind’s hidden complexities, 2002) from cognitive linguistics describes how one constructs meaning from various stimuli, such as text and diagrams, through conceptual integration or blending. The conceptual integration networks that describe the conceptual integration process characterize cognition that occurs unconsciously during meaning construction. These same networks are used to describe some of the cognition while resolving an anomaly in molecular genetics called RNA interference (RNAi) in a case study. The RNAi case study is a cognitive-historical reconstruction (Nersessian, In: Giere (ed) Cognitive models of science, 1992) that reconstructs how the RNAi anomaly was resolved. This reconstruction traces four relevant molecular genetics publications in describing the cognition necessary in accounting for how RNAi was resolved through strategies (Darden 1991), abductive reasoning (Peirce, In: Hartshorne, Weiss (eds) Collected papers, 1958), and experimental reasoning (Gooding 1990). The results of the case study show that experiments play a crucial role in formulating an explanation of the RNAi anomaly and the integration networks describe the experiments’ role. Furthermore, these results suggest that RNAi anomaly resolution is embodied. It is embodied in a sense that cognition described in the cognitive-historical reconstruction is experientially based. (shrink)

Several recent results bring into focus the superintuitionistic nature of most notions of proof-theoretic validity, but little work has been done evaluating the consequences of these results. Proof-theoretic validity claims to offer a formal explication of how inferences follow from the definitions of logic connectives (which are defined by their introduction rules). This paper explores whether the new results undermine this claim. It is argued that, while the formal results are worrying, superintuitionistic inferences are valid because the treatments (...) of atomic formulas are insufficiently general, and a resolution to this issue is proposed. (shrink)

We propose a simple and intuitive algorithm for solving md-DFA problem using algorithm concepts within extended operators, our approach shows quadratic polynomial time and hence proves the equivalence between polynomial and non-polynomial classes, we have also shown that minimal non-emptiness of automata problem can be solved in polynomial time with help of modified subset construction, rather that building a product automaton, which lead to factorial size of the memory and time, in this work we also have used many non-tractable existing (...) examples and computed them in polynomial time, which guarantees that our algorithm solves NP-complete problem in almost linear polynomial time, we have also avoided the problem of product automata by an algorithmic approach, we are also giving the starting ground for the proof of back-reference problem which was discussed before, notion to the globally local increment is also given as the main argument towards the resolution of "P versus NP" theorem, which coincides with the finitarity term in general mathematics. (shrink)

This paper provides a logical proof of the non-existence of “infinity” within the hierarchy of physical reality, grounded in the laws of thermodynamics and information theory. Building upon the author’s previous definition of existence as difference (Saito, 2025), I demonstrate that the maintenance of any such difference requires a minimum thermodynamic energy cost, as dictated by Landauer’s Principle. Given that the total energy of the universe is finite, the number of definable differences is necessarily capped at a physical upper (...) bound. Consequently, infinity cannot manifest as an actual entity within the realm of physical existence. Furthermore, this proof is applied to resolve the Continuum Hypothesis (CH) by illustrating how the fundamental resolution of physical space (Planck scale) renders questions of infinite cardinality moot. I conclude by re-defining the universe as a dynamic computing system with finite resources, establishing the logical foundation for the Principle of Mutual Optimization to be detailed in subsequent works. (shrink)

A Ramsey statement denoted \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${n \longrightarrow (k)^2_2}$$\end{document} says that every undirected graph on n vertices contains either a clique or an independent set of size k. Any such valid statement can be encoded into a valid DNF formula RAM(n, k) of size O(nk) and with terms of size \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\left(\begin{smallmatrix}k\\2\end{smallmatrix}\right)}$$\end{document}. Let rk be the minimal n for which the statement holds. We prove that (...) RAM(rk, k) requires exponential size constant depth Frege systems, answering a problem of Krishnamurthy and Moll [15]. As a consequence of Pudlák’s work in bounded arithmetic [19] it is known that there are quasi-polynomial size constant depth Frege proofs of RAM(4k, k), but the proof complexity of these formulas in resolution R or in its extension R(log) is unknown. We define two relativizations of the Ramsey statement that still have quasi-polynomial size constant depth Frege proofs but for which we establish exponential lower bound for R. (shrink)

A proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) with k inferences has an interpolant whose circuit-size is at most k. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it (...) several corollaries: (1) Feasible interpolation theorems for the following proof systems: (a) resolution (b) a subsystem of LK corresponding to the bounded arithmetic theory S 2 2 (α) (c) linear equational calculus (d) cutting planes. (2) New proofs of the exponential lower bounds (for new formulas) (a) for resolution ([15]) (b) for the cutting planes proof system with coefficients written in unary ([4]). (3) An alternative proof of the independence result of [43] concerning the provability of circuit-size lower bounds in the bounded arithmetic theory S 2 2 (α). In the other direction we show that a depth 2 subsystem of LK does not admit feasible monotone interpolation theorem (the so called Lyndon theorem), and that a feasible monotone interpolation theorem for the depth 1 subsystem of LK would yield new exponential lower bounds for resolution proofs of the weak pigeonhole principle. (shrink)

By analyzing what are necessary conditions in the proof [4] ofthe classical model existence theorem CME, we present the left resolution Gentzen systems R,which proof-theoretically characterize CME.

The relation of normic support offers a novel solution to the proof paradox: a paradox in evidence law arising from legal cases involving merely statistical evidence (Smith 2018). Central to the normic support solution has been the thesis that merely statistical evidence cannot confer normic support. However, it has been observed that there are exceptions to this: there exist cases where merely statistical evidence can give rise to normic support (Blome-Tillmann 2020). If correct, this fact seems to undermine the (...) normic support solution to the proof paradox. This paper explores a resolution: normic support can resolve the proof paradox even though merely statistical evidence sometimes gives rise to normic support. The key to understanding this resolution lies with a source of evidential support that arises out of bodies of evidence that involve *character evidence* (Colyvan, et al. 2001). It turns out that character evidence can provide normic support when it is grounded in our knowledge of a certain kind of disposition individuals can have: *goal-directed dispositions*. The upshot is the recovery of the normic support solution to the puzzle of whether statistical evidence can meet legal standards of proof. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Journal of the History of Ideas 64.4 (2003) 599-618 [Access article in PDF] The "Herbert Butterfield Problem" and its Resolution Keith C. Sewell Dordt College Herbert Butterfield (1900-1979) 1 published The Whig Interpretation of History in 1931, a year after he became a Lecturer in the University of Cambridge. 2 He became Professor of Modern History in the university in 1944, the same year in which he published (...) The Englishman and His History. 3 This discussion addresses what J.G.A. Pocock referred to as das Herbert Butter-fieldproblem—that is, the problem of ascertaining the precise relationship between the arguments presented in these volumes. 4The Whig Interpretation of History of 1931 (hereafter, The Whig Interpretation) was a sustained critique of the motivation, methods and fallacious conclusions of the "Whig" practice of staging historiographical narratives anachronistically so as to produce a ratification of the present, or justification of a position currently espoused by the author. 5 The term "Whig," as Butterfield used it in 1931, referred to the nineteenth-century school of historiography that praised "progress," "protestantism," and "liberty" and that generally attributed the triumph of such principles to the beliefs and activities of generations of Whig politicians. 6 [End Page 599]The Whig Interpretation argued that the judgments concerning both progressive and reactionary individuals and movements in Whig historiography were anachronistic, in that they were based on general propositions held by the Whig historian in the present. To correct this error Butterfield argued that historiography should not be based upon any general propositions. Basing historiographical narratives on general propositions purporting to be of universal and unchanging validity was seen as inevitably placing them on an anachronistic basis. In The Whig Interpretation Butterfield required the historian to represent past "life itself " but to avoid doing so on the basis of a view or "interpretation" of past human experience and action. Historiographical narration should be free of any interpretative standpoint and equally open to any possible subsequent interpretation. For Butterfield "the historian carries us away from the world of general ideas. It is not for him to give a philosophical explanation of what happens in time and space"; "any history that he writes ought to be as capable of varied philosophical interpretation as life itself seems to be... the historian's explanation... is not a piece of general reasoning," and "if at any point we need further elucidation all that he can do is to take us into greater detail." 7 It seems appropriate to refer to this as Butterfield's "neutrality postulate." Butterfield subsequently used the term "technical history" to denote this methodological concept. 8As might be expected, such a neutrality postulate was replete with problems, however valid Butterfield's strictures towards Whig historiographical anachronism. How is the historian to abridge for the purposes of narration and explanation without interpreting? Butterfield argued that we are right to demand of the historian that "he shall not change the meaning and purport of the historical story in the mere act of abridging it." No theory should intrude. As the detailed complexity is abridged, there should be no loss of "the purport and tenor of the whole." 9 Abridgment was to be accomplished without interpretative perspective, even though sympathy and imagination are indispensable. 10 Such was Butterfield's prescribed antidote. Yet the exercise he recommended requires more than a specific statement of the concrete, the individual, and the particular. It also requires a general idea of the "meaning" of "the whole" that the historian is called upon not to distort. Indeed, Butterfield drew attention to the basis of his historical thinking when he asserted that while historical research does not provide proof of the existence of a providential order, it nevertheless provides evidence of how profound and mysterious are its workings. 11In The Whig Interpretation no attempt was made to reconcile the advocacy of a non-interpretative neutrality dealing exclusively with the individual, the [End Page 600] concrete and the particular, and Butterfield's actual belief in a providential order to which the historical process is subject. After 1931... (shrink)

We study the complexity of proving the Pigeon Hole Principle in a monotone variant of the Gentzen Calculus, also known as Geometric Logic. We prove a size-depth trade-off upper bound for monotone proofs of the standard encoding of the PHP as a monotone sequent. At one extreme of the trade-off we get quasipolynomia -size monotone proofs, and at the other extreme we get subexponential-size bounded-depth monotone proofs. This result is a consequence of deriving the basic properties of certain monotone formulas (...) computing the Boolean threshold functions. We also consider the monotone sequent expressing the Clique-Coclique Principle defined by Bonet, Pitassi and Raz [9]. We show that monotone proofs for this sequent can be easily reduced to monotone proofs of the one-to-one and onto PHP, and so CLIQUE also has quasipolynomia -size monotone proofs. As a consequence of our results, Resolution, Cutting Planes with polynomially bounded coefficients, and Bounded-Depth Frege are exponentially separated from the monotone Gentzen Calculus. Finally, a simple simulation argument implies that these results extend to the Intuitionistic Gentzen Calculus. Our results partially answer some questions left open by P. Pudlák. (shrink)

We provide a number of simplified and improved separations between pairs of Resolution-with-bounded-conjunction refutation systems, Res, as well as their tree-like versions, Res⁎. The contradictions we use are natural combinatorial principles: the Least number principle, LNPn and an ordered variant thereof, the Induction principle, IPn.LNPn is known to be easy for Resolution. We prove that its relativization is hard for Resolution, and more generally, the relativization of LNPn iterated d times provides a separation between Res and Res. (...) We prove the same result for the iterated relativization of IPn, where the tree-like variant Res⁎ is considered instead of Res.We go on to provide separations between the parameterized versions of Res and Res. Here we are able again to use the relativization of the LNPn, but the classical proof breaks down and we are forced to use an alternative. Finally, we separate the parameterized versions of Res⁎ and Res⁎. Here, the relativization of IPn will not work as it is, and so we make a vectorizing amendment to it in order to address this shortcoming. (shrink)

This study seeks to advance the understanding of controversy resolution in science. I take as a case study conceptualization and treatment of ulcer disease. Analysis of causal accounts and effective treatments illustrate the ways in which competing parallel research programs in medicine embody opposing social, political, and economic forces which are bound to the epistemological dimensions of scientific controversy (e.g., standards of evidence, reference, and inference), and which in turn shift perception of the burden of proof. The analysis (...) illustrates the ways in which (1) medical diagnoses create as much as discover useful distinctions and (2) epistemic and non epistemic values divide scientists into competing research programs, as well as (3) the ways in which these structures often effectively prevent scientific controversy closure. (shrink)

During the latter part of the nineteenth century our description of nerve cell structure underwent a relatively unrecognized, though fundamental, transformation-a quiet revolution of sorts. The central problem facing scientists in neurology (the study of the nervous system) was a related pair: are nerve cells continuous with each other or not, and how is information conducted? Microscope resolution and staining techniques were inadequate at the time to yield definitive proof either way. I contend that explanatory coherence provides a (...) means to elucidate this instance of theory change in the history of science. The means of elucidation will be Thagard's computational model of explanatory coherence, ECHO (). (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Proof and Persuasion in the Philosophical Debate about AbortionChris KaposyPhilosophers involved in debating the abortion issue often assume that the arguments they provide can offer decisive resolution.1 Arguments on the prolife side of the debate, for example, usually imply that it is rationally mandatory to view the fetus as having a right to life, or full moral standing.2 Such an account assumes that philosophical argument can compel (...) the reader to see the fetus in a certain way and that dissent risks irrationality.I wish to question this image of the use of philosophical argument in the abortion debate. I focus on the question of fetal moral standing, which is one of the subproblems in the debate. I am especially concerned with prolife arguments for fetal moral standing, since the prolife side must argue for a position that is compulsory. The prochoice side, in contrast, typically holds that people are entitled to believe what they want about the fetus’s moral standing.My position is that philosophical arguments should be understood as tools for persuasion in the abortion debate rather than as a method for discovering decisive proofs about the morality of abortion. I argue that because any one position on the moral standing of fetuses cannot be established decisively, law and policy should favour the prochoice position. In support of these conclusions, I present two common argumentative strategies used to suggest that the prolife view of the fetus is rationally [End Page 139] mandatory, and I illustrate why arguments involving these strategies do not compel us to view the fetus as having full moral standing.Framing the IssueIn order to show that abortion is wrong (in cases in which it is considered wrong), one must first establish that fetuses have full moral standing.3 It is a serious moral wrong to take the life of someone with full moral standing—this is part of what it means to have this status. The possessor of full moral standing is entitled to have his or her life protected. If abortion is wrong, then the fetus must have full moral standing, because without such standing, killing a fetus could be justified by the pregnant woman’s strong interest in ending an unwanted pregnancy. Those arguing against the moral permissibility of abortion must show that it is mandatory (in some way) to view the fetus as having full moral standing. There are a range of positions one could take with regard to the fetus’s status, from viewing the fetus as an incipient organism with no moral standing to seeing the fetus as gaining moral standing as the pregnancy progresses. But if it is mandatory to view the fetus as having full moral standing, all other positions must then be mistaken, incorrect, or somehow unjustified.This paper analyzes why philosophers opposed to abortion think it is mandatory to attribute full moral standing to fetuses. There are two popular argumentative strategies offering different accounts of the source of this obligation. The first strategy suggests that fetal full moral standing derives from morally relevant facts about the fetus. According to this line of argument, we are rationally obligated to view the fetus as having full moral standing because we cannot deny (without courting irrationality) that there are properties, characteristics, or attributes of the fetus that entitle it to this status.The second strategy is to claim that the fetus has full moral standing because this position is most consistent with our intuitions in cases unrelated to abortion. Philosophers taking this approach are fond of analogies comparing fetuses to comatose adults or to people at the end of life, for example. This strategy of appealing to your interlocutor’s sense of consistency I call the “shared-value” strategy.The two strategies map very well onto the distinction some have made between argumentum ad rem and argumentum ad hominem. The philosopher of rhetoric Henry Johnstone Jr. draws this distinction in very clear terms, and others in the history of philosophy make note of the difference [End Page 140] between these two types of arguments as well.4 The appeal to the facts (or argumentum ad rem) seeks to establish the truth of its... (shrink)

Uniform proofs systems have recently been proposed [Mi191j as a proof-theoretic foundation and generalization of logic programming. In [Mom92a] an extension with constructive negation is presented preserving the nature of abstract logic programming language. Here we adapt this approach to provide a complete theorem proving technique for minimal, intuitionistic and classical logic, which is totally goal-oriented and does not require any form of ancestry resolution. The key idea is to use the Godel-Gentzen translation to embed those logics in (...) the syntax of Hereditary Harrop formulae, for which uniform proofs are complete. We discuss some preliminary implementation issues. (shrink)

herent and rational way. Several proposals have been made for information merging in which it is possible to encode the preferences of sources (Benferhat, Dubois, Prade, & Williams, 1999; Benferhat, Dubois, Kaci, & Prade, 2000; Lafage & Lang, 2000; Meyer, 2000, 2001; Andreka, Ryan, & Schobbens, 2001). Information merging has much in common with social choice theory, which aims to define operations reflecting the preferences of a society from the individual preferences of the members of the society. Given this connection, (...) frameworks for information merging should provide satisfactory resolutions of problems raised in social choice theory. We investigate the link between the merging of epistemic states and two important results in social choice theory. We show that Arrow’s well-known impossibility theorem (Arrow, 1963) does not hold in merging frameworks when the preferences of sources are represented in terms of epistemic states. This is achieved by providing a consistent set of properties for merging from which Arrow-like properties can be derived. Similarly, by extending these to a consistent framework which includes properties corresponding to the notion of being strategy-proof, we show that results due to Gibbard and Satterthwaite (Gibbard, 1973; Satterthwaite, 1973, 1975) and other (Benoit, 2000; Barber´a, Dutta, & Sen, 2000) do not hold in merging frameworks. (shrink)

This paper is a continuation of dag-like proof compression research initiated in [9]. We investigate proof compression phenomenon in a particular, most transparent case of propositional DNF Logic. We define and analyze a very efficient semi-analytic sequent calculus SEQ*0 for propositional DNF. The efficiency is achieved by adding two special rules CQ and CS; the latter rule is a variant of the weakened substitution rule WS from [9], while the former one being specially designed for DNF sequents. We (...) show that dag-like SEQ*0 has good deterministic proof search strategy. Furthermore, we expose six examples showing that dag-like deducibility in SEQ*0 admits exponential-size proof compression, as compared to familiar proof systems like cutfree sequent calculi, resolution and cutting plane proof systems. (shrink)

Cook and Reckhow defined a propositional formulation of the pigeonhole principle. This paper shows that there are Frege proofs of this propositional pigeonhole principle of polynomial size. This together with a result of Haken gives another proof of Urquhart's theorem that Frege systems have an exponential speedup over resolution. We also discuss connections to provability in theories of bounded arithmetic.

We consider the task of theorem proving in Lambek calculi and their generalisation to ‘multimodal residuation calculi’. These form an integral part of categorial logic, a logic of signs stemming from categorial grammar, of the basis of which language processing is essentially theorem proving. The demand of this application is not just for efficient processing of some or other specific calculus, but for methods that will be generally applicable to categorial logics.It is proposed that multimodal cases be treated by dealing (...) with the highest common factor of all the connectives as linear validity. The prosodic aspects are encoded in labels, in effect the term-structure of quantified linear logic. The correctness condition on proof nets can be implemented by SLD resolution in linear logic with unification on labels/terms limited to one way matching. A suitable unification strategy is obtained for calculi of discontinuity by normalisation of the ground goal term followed by recursive descent and redex pattern matching on the head term. (shrink)

Edgar Wind was one of the most distinguished art historians and philosophers of the twentieth century. He made crucial contributions to debates on aesthetics and on the interdisciplinary nature of cultural history involving such other leading figures as Ernst Cassirer and Erwin Panofsky. It is not always realised, however, that his early thinking was moulded by a concern with the German philosophical tradition, culminating in the analysis of the meaning and function of scientific experimentation and proof. This first edition (...) in English of Edgar Wind's important work Das Experiment und die Metaphysik: Zur Auflosung der kosmologischen Antinomien (1934) also carries a new introduction by Matthew Rampley, placing Wind's philosophical thinking in context. The work is being published to coincide with the opening in 2000 of the Sackler Library at Oxford, which will include a Wind Reading Room. (shrink)

We prove that the problem of determining the minimum propositional proof length is NP- hard to approximate within a factor of 2 log 1 - o(1) n. These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution, Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof (...) length measured either by number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problems of approximation of the length of proofs. (shrink)

This paper consists in an exposition of a proof Newton gave in 1666 of the parallelogram law for compounding velocities, and an examination of its implications for understanding his treatment of motion resulting from a continuously acting force in the Principia. I argue that the “moments” invoked in the fluxional proof of the vector resolution and composition of velocities are “virtual times”, a device allowing Newton to represent motions by the linear displacements produced in such a time; (...) the ratio of velocities at an instant can then be represented by assuming the velocities continue for such a virtual time. By the Method of First and Ultimate Ratios, the first ratio of the velocities is then given by the ratio of such lines, under the presupposition that in the limit they will shrink to zero magnitude. I then argue that the same device is implicit in Newton’s appeal to “moments” or “particles of time” in his proof of Kepler’s Area Law in the “Locke Paper” and in Proposition 1 of Book 1 of the Principia, and that the limiting process involved there is therefore the same as that implicit in the Method of First and Ultimate Ratios. (shrink)

ABSTRACT In this paper we state and prove Herbrand's properties for two modal systems, namely T and S4, thus adapting a previous result obtained for the system D [CIA 86a] to such theories. These properties allow the first order extension—along the lines of [CIA 91]—of the resolution method defined in [ENJ 86] for the corresponding propositional modal systems. In fact, the Herbrand-style procedures proposed here treat quantifiers in a uniform way, that suggests the definition of a restricted notion of (...) unification for quantifier free modal formulae obtained by means of a Skolem-like procedure. The differences among the three systems considered, D, T and S4, are taken into account by preliminary propositional transformations of the formulae, in such a way that the problem of quantifier elimination can be treated within the same pattern in the different systems. The methods employed to prove the fundamental theorems are purely proof-theoretical and make use of the formalization of the considered modal theories in terms of sequent calculi, where the cut elimination theorem holds. (shrink)

"We argue that the computation of a logic program can be usefully divided into two distinct phases: the first being a proof- valued computation or proof-search; the second a residual computation, or answer extraction. Extension of extraction techniques to various theories then permits more extensive languages and proof procedures to be employed for the computational solution of problems. We illustrate these ideas with a simple propositional logic and show that SLD-resolution computes presentations of proofs in which (...) the residual computation may be interleaved with the proof-search, whereas a more general proof procedure yields shorter presentations of (the same) proofs, but which require more extensive residual computations.". (shrink)

In this paper, I develop a quasi-transcendental argument to justify Kant’s infamous claim “man is evil by nature.” The cornerstone of my reconstruction lies in drawing a systematic distinction between the seemingly identical concepts of “evil disposition” (böseGesinnung) and “propensity to evil” (Hang zumBösen). The former, I argue, Kant reserves to describe the fundamental moral outlook of a single individual; the latter, the moral orientation of the whole species. Moreover, the appellative “evil” ranges over two different types of moral failure: (...) while an “evil disposition” is a failure to realize the good (i.e., to adopt the motive of duty as limiting condition for all one’s desires), an “evil propensity” is a failure to realize the highest good (i.e., to engage in the collective project of transforming the legal order into an ethical community). This correlation between units of moral analysis and types of obligation suggests a way to offer a deduction of the universal propensity on behalf of Kant. It consists in tracing the source of radical evil to the same subjective necessity that gives rise to the doctrine of the highest good. For, at the basis of Kant’s two doctrines lies the same natural dialectic between happiness and morality. While the highest good brings about the critically acceptable resolution of this dialectic, the propensity to evil perpetuates and aggravates it. Instead of connecting happiness and morality in an objective relation, the human will subordinatesmorality to the pursuit of happiness according to the subjective order of association. If this reading is correct, it would explain why prior attempts at a transcendental deduction have failed: interpreters have looked for the key to the deduction in the body of Kant’s text, where it is not to be found, for it is tucked, instead, in the Preface to the first edition. (shrink)

We prove an exponential lower bound on the size of proofs in the proof system operating with ordered binary decision diagrams introduced by Atserias, Kolaitis and Vardi [2]. In fact, the lower bound applies to semantic derivations operating with sets defined by OBDDs. We do not assume any particular format of proofs or ordering of variables, the hard formulas are in CNF. We utilize (somewhat indirectly) feasible interpolation. We define a proof system combining resolution and the OBDD (...) proof system. (shrink)

The goal of this article is to take a step toward the resolution of the problem of finding an analytic sequent calculus for the logic of proofs. For this, we focus on the system Ilp, the intuitionistic version of the logic of proofs. First we present the sequent calculus Gilp that is sound and complete with respect to the system Ilp; we prove that Gilp is cut-free and contraction-free, but it still does not enjoy the subformula property. Then, we (...) enrich the language of the logic of proofs and we formulate in this language a second Gentzen calculus Gilp∗. We show that Gilp∗ is a conservative extension of Gilp, and that Gilp∗ satisfies the subformula property. (shrink)