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)

We introduce a notion of relative efficiency for axiom systems. Given an axiom system Aβ for a theory T consistent with S12, we show that the problem of deciding whether an axiom system Aα for the same theory is more efficient than Aβ is II2-hard. Several possibilities of speed-up of proofs are examined in relation to pairs of axiom systems Aα, Aβ, with Aα ⊇ Aβ, both in the case of Aα, Aβ having the same language, and in (...) the case of the language of Aα extending that of Aβ: in the latter case, letting Prα, Prβ denote the theories axiomatized by Aα, Aβ, respectively, and assuming Prα to be a conservative extension of Prβ, we show that if Aα — Aβ contains no nonlogical axioms, then Aα can only be a linear speed-up of Aβ; otherwise, given any recursive function g and any Aβ, there exists a finite extension Aα of Aβ such that Aα is a speed-up of Aβ with respect to g. (shrink)

In order to develop efficient tools for automated reasoning with inconsistency (theorem provers), eventually making Logics of Formal inconsistency (_LFI_) a more appealing formalism for reasoning under uncertainty, it is important to develop the proof theory of the first-order versions of such _LFI_s. Here, we intend to make a first step in this direction. On the other hand, the logic _Ciore_ was developed to provide new logical systems in the study of inconsistent databases from the point of view of _LFI_s. (...) An interesting fact about _Ciore_ is that it has a _strong_ consistency operator, that is, a consistency operator which (forward/backward) propagates inconsistency. Also, it turns out to be an algebraizable logic (in the sense of Blok and Pigozzi) that can be characterized by means of a 3-valued logical matrix. Recently, a first-order version of _Ciore_, namely _QCiore_, was defined preserving the spirit of _Ciore_, that is, without introducing unexpected relationships between the quantifiers. Besides, some important model-theoretic results were obtained for this logic. In this paper we study some proof–theoretic aspects of both _Ciore_ and _QCiore_ respectively. In first place, we introduce a two-sided sequent system for _Ciore_. Later, we prove that this system enjoys the cut-elimination property and apply it to derive some interesting properties. Later, we extend the above-mentioned system to first-order languages and prove completeness and cut-elimination property using the well-known Shütte’s technique. (shrink)

Symlog is a system for learning symbolic logic by computer that allows students to interactively construct proofs in Fitch-style natural deduction. On request, Symlog can provide guidance and advice to help a student narrow the gap between goal theorem and premises. To effectively implement this capability, the program was equipped with a theorem prover that constructs proofs using the same methods and techniques the students are being taught. This paper discusses some of the aspects of the theorem prover's (...) design, including its set of proof-construction strategies, its unification algorithm as well as some of the tradeoffs between efficiency and pedagogy. (shrink)

We introduce an Automatic Theorem Prover (ATP) of a dual tableau system for a relational logic for order of magnitude qualitative reasoning, which allows us to deal with relations such as negligibility, non-closeness and distance. Dual tableau systems are validity checkers that can serve as a tool for verification of a variety of tasks in order of magnitude reasoning, such as the use of qualitative sum of some classes of numbers. In the design of our ATP, we have introduced some (...) heuristics, such as the so called phantom variables, which improve the efficiency of the selection of variables used un the proof. (shrink)

We present a sequent calculus with the Henkin constants in the place of the free variables. By disposing of the eigenvariable condition, we obtained a proof system with a strong locality property—the validity of each inference step depends only on its active formulas, not its context. Our major outcomes are: the cut elimination via a non-Gentzen-style algorithm without resorting to regularization and the elimination of Skolem functions with linear increase in the proof length for a subclass of derivations with cuts.

The price of Bitcoin is once more soaring. From early October 2020 to early January 2021, the price of a single Bitcoin token went from roughly $10,000 to nearly $65,000, reinspiring the hopes of the crypto-faithful in the inevitability of a future beyond centralized banking and leaving the rest to dread the jargon of computational libertarianism. The speculative betting driving this recent price action, however, belies a more rudimentary and overlooked shift in the digital economy signaled by cryptocurrencies and Bitcoin (...) in particular. Unlike an earlier industrial logic that sought to reduce heat loss and improve efficiency to maximize surplus value, Bitcoin’s proof-of-work system shifts the basis of value production from efficiency to inefficiency. Moreover, it does so by using a cryptographic algorithm whose purpose is to destroy the meaning of its inputs. Through an exploration of Bitcoin’s proof-of-work technics and its inversion of traditional models of value extraction, the text argues that Bitcoin reveals a profound transformation in the nature of surplus represented by computational capitalism. (shrink)

A previously unexplored method, combining logical and mathematical elements, is shown to yield substantial numerical improvements in the area of Diophantine approximations. Kreisel illustrated the method abstractly by noting that effective bounds on the number of elements are ensured if Herbrand terms from ineffective proofs ofΣ2-finiteness theorems satisfy certain simple growth conditions. Here several efficient growth conditions for the same purpose are presented that are actually satisfied in practice, in particular, by the proofs of Roth's theorem due to (...) Roth himself and to Esnault and Viehweg. The analysis of the former yields an exponential bound of order exp in place of exp given by Davenport and Roth in 1955, whereαis algebraic of degreed≥ 2 and ∣α−pq−1∣ shrink)

The epistemic position of an agent often depends on their position in a larger network of other agents who provide them with information. In general, agents are better off if they have diverse and independent sources. Sullivan et al. [19] developed a method for quantitatively characterizing the epistemic position of individuals in a network that takes into account both diversity and independence; and presented a proof-of-concept, closed-source implementation on a small graph derived from Twitter data [19]. This paper reports on (...) an open-source reimplementation of their algorithm in Python, optimized to be usable on much larger networks. In addition to the algorithm and package, we also show the ability to scale up our package to large synthetic social network graph profiling, and finally demonstrate its utility in analyzing real-world empirical evidence of ‘echo chambers’ on online social media, as well as evidence of interdisciplinary diversity in an academic communications network. (shrink)

Fuzzy logics are many-valued logics that are well suited to reasoning in the context of vagueness. They provide the basis for the wider field of Fuzzy Logic, encompassing diverse areas such as fuzzy control, fuzzy databases, and fuzzy mathematics. This book provides an accessible and up-to-date introduction to this fast-growing and increasingly popular area. It focuses in particular on the development and applications of "proof-theoretic" presentations of fuzzy logics; the result of more than ten years of intensive work by researchers (...) in the area, including the authors. In addition to providing alternative elegant presentations of fuzzy logics, proof-theoretic methods are useful for addressing theoretical problems and developing efficient deduction and decision algorithms. Proof-theoretic presentations also place fuzzy logics in the broader landscape of non-classical logics, revealing deep relations with other logics studied in Computer Science, Mathematics, and Philosophy. The book builds methodically from the semantic origins of fuzzy logics to proof-theoretic presentations such as Hilbert and Gentzen systems, introducing both theoretical and practical applications of these presentations. (shrink)

Can God be the efficient cause of himself (causa sui,)? It is well known that Descartes answers this question in the affirmative, but it is considerably less clear why. The main contention of the essay is that Descartes advances the causa sui doctrine because he came to think that the ontological proof of Meditation V required it. We argue these contentions through a close analysis of Descartes' initial articulation of causa sui in response to Caterus, followed by attention to the (...) reformulation of the doctrine in response to the logical objections posed by Arnauld. Our understanding of causa sui as a move made within the horizon of the ontological proof not only illuminates why Descartes would have defended a doctrine as conceptually problematic as causa sui, but also provides an alternative to Jean-Luc Marion's view that causa sui constitutes a third, distinct proof for the existence of God. /// Pode Deus ser a causa eficiente de si mesmo (causa sui,)? É bem sabido que Descartes responde aflrmativamente a esta questão, mas é consideravelmente menos claro porquê. O principal conteúdo do ensaio é que Descartes apresenta a doutrina da causa sui porque pensou que a prova ontológica da Meditação V precisava dela. Demonstramos estas afirmações através de uma análise rigorosa da articulação inicial de Descartes da causa sui em resposta a Caterus, seguida de uma atenção à reformulação da doutrina em resposta às objecções logicas apresentadas por Arnauld. A nossa compreensão da causa sui como proposta feita no horizonte da prova ontológica não ilumina apenas porque é que Descartes teria defendido uma doutrina conceptualmente tão problemática como a causa sui, mas também providencia uma alternativa ao ponto de vista de Jean-Luc Marion de que a causa sui constitui a terceira, prova distintapara a existência de Deus. (shrink)

Edward Feser defends the ‘Neo-Platonic proof ’ for the existence of the God of classical theism. After articulating the argument and a number of preliminaries, I first argue that premise three of Feser’s argument—the causal principle that every composite object requires a sustaining efficient cause to combine its parts—is both unjustified and dialectically ill-situated. I then argue that the Neo-Platonic proof fails to deliver the mindedness of the absolutely simple being and instead militates against its mindedness. Finally, I uncover two (...) tensions between Trinitarianism and the Neo-Platonic proof. (shrink)

A lengthy argument for the existence of a being possessing most of the attributes ascribed to God in traditional philosophical theology is set forth by John Duns Scotus in the final two chapters of his Tractatus De Primo Principio.1 In 3.1-19, Scotus tries to establish the core of his proof, viz., that "an absolutely first effective is actually existent." It is an ingenious blend of elements that figure in standard versions of the cosmological and ontological arguments. However, while the reader (...) of De Primo is apt to be deeply intrigued by the suggestiveness and originality of Scotus' discussion, attempting to organize and interpret the various threads of argument is a challenging task. This no doubt partially explains the relative neglect of Scotus' argument in contemporary discussion of theistic proofs. In what follows, I offer a reading of the argument as well as my critical assessment of it. I will contend that Scotus is unable to achieve all that he wants, in that a critical aspect of his official version of the argument is centrally flawed. However, the text also seems to suggest a modified version of the proof which relies on intuitive support for a possibility claim. I maintain that this form of the proof is sound. Furthermore, owing to the comparative weakness of its underived premises, Scotus' proof can be seen to offer a novel and appealing alternative to the more widely advertised versions of the cosmological and ontological arguments. If I am right, then, Scotus' De Primo has an important contribution to make to the contemporary discussion of an issue of perennial philosophical concern. (shrink)

Mathematicians judge proofs to possess, or lack, a variety of different qualities, including, for example, explanatory power, depth, purity, beauty and fit. Philosophers of mathematical practice have begun to investigate the nature of such qualities. However, mathematicians frequently draw attention to another desirable proof quality: being motivated. Intuitively, motivated proofs contain no "puzzling" steps, but they have received little further analysis. In this paper, I begin a philosophical investigation into motivated proofs. I suggest that a proof is (...) motivated if and only if mathematicians can identify (i) the tasks each step is intended to perform; and (ii) where each step could have reasonably come from. I argue that motivated proofs promote understanding, convey new mathematical resources and stimulate new discoveries. They thus have significant epistemic benefits and directly contribute to the efficient dissemination and advancement of mathematical knowledge. Given their benefits, I also discuss the more practical matter of how we can produce motivated proofs. Finally I consider the relationship between motivated proofs and proofs which are explanatory, beautiful and fitting. (shrink)

This paper introduces and describes new protocols for proving knowledge of secrets without giving them away: if the verifier does not know the secret, he does not learn it. This can all be done while only using one-way hash functions. If also the use of encryption is allowed, these goals can be reached in a more efficient way. We extend and use the GNY authentication logic to prove correctness of these protocols.

Public entities around the world are increasingly deploying artificial intelligence and algorithmic decision-making systems to provide public services or to use their enforcement powers. The rationale for the public sector to use these systems is similar to private sector: increase efficiency and speed of transactions and lower the costs. However, public entities are first and foremost established to meet the needs of the members of society and protect the safety, fundamental rights, and wellbeing of those they serve. Currently AI (...) systems are deployed by the public sector at various administrative levels without robust due diligence, monitoring, or transparency. This paper critically maps out the challenges in procurement of AI systems by public entities and the long-term implications necessitating AI-specific procurement guidelines and processes. This dual-prong exploration includes the new complexities and risks introduced by AI systems, and the institutional capabilities impacting the decision-making process. AI-specific public procurement guidelines are urgently needed to protect fundamental rights and due process. (shrink)

Proof and Consequence is a rigorous, elegant introduction to classical first-order natural deductive logic; it provides an accurate and accessible first course in the study of formal systems. The text covers all the topics necessary for learning logic at the beginner and intermediate levels: this includes propositional and quantificational logic (using Suppes-style proofs) and extensive metatheory, as well as over 800 exercises. Proof and Consequence provides exclusive access to the software application Simon, an easily downloadable program designed to facilitate (...) an intuitive understanding of classical logic through the generation and analysis of proofs. It also aids with the representation of natural language sentences in the formal language. Equipped with nearly all the exercises found in the text, Simon helps students work efficiently and effectively by detecting and explaining errors in solutions as they proceed. Students can also submit assignments, view their own records, and check their standing in the class. The complete logic package includes: * The logic textbook, Proof and Consequence *A very helpful study guide to the textbook, containing extra exercises, Simple Simon *Access, through Simon, to the grading software, Simon Says, that allows students to submit assignments and track their grades. (shrink)

Recently, philosophers and social scientists have turned their attention to the epistemological shifts provoked in established sciences by their incorporation of big data techniques. There has been less focus on the forms of epistemology proper to the investigation of algorithms themselves, understood as scientific objects in their own right. This article, based upon 12 months of ethnographic fieldwork with Russian data scientists, addresses this lack through an investigation of the specific forms of epistemic attention paid to algorithms by data scientists. (...) On the one hand, algorithms are unlike other mathematical objects in that they are not subject to disputation through deductive proof. On the other hand, unlike concrete things in the world such as particles or organisms, algorithms cannot be installed as the objects of experimental systems directly. They can only be evaluated in their functioning as components of extended computational assemblages; on their own, they are inert. As a consequence, the epistemological coding proper to this evaluation does not turn on truth and falsehood but rather on the efficiency of a given algorithmic assemblage. This article suggests that understanding the forms of algorithmic rationality employed in such inquiry is crucial for charting the place of data science within the contemporary academy and knowledge economy more generally. (shrink)

The formulas-as-types isomorphism tells us that every proof and theorem, in the intuitionistic implicational logic $H_\rightarrow$, corresponds to a lambda term or combinator and its type. The algorithms of Bunder very efficiently find a lambda term inhabitant, if any, of any given type of $H_\rightarrow$ and of many of its subsystems. In most cases the search procedure has a simple bound based roughly on the length of the formula involved. Computer implementations of some of these procedures were done in Dekker. (...) In this paper we extend these methods to full classical propositional logic as well as to its various subsystems. This extension has partly been implemented by Oostdijk. (shrink)

We describe a relational framework that uniformly supports formalization and automated reasoning in varied propositional modal logics. The proof system we propose is a relational variant of the classical Rasiowa-Sikorski proof system. We introduce a compact graph-based representation of formulae and proofs supporting an efficient implementation of the basic inference engine, as well as of a number of refinements. Completeness and soundness results are shown and a Prolog implementation is described.

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)

Basic hybrid logic extends modal logic with the possibility of naming worlds by means of a distinguished class of atoms (called nominals) and the so-called satisfaction operator, that allows one to state that a given formula holds at the world named a, for some nominal a. Hence, in particular, hybrid formulae include “equality” assertions, stating that two nominals are distinct names for the same world. The treatment of such nominal equalities in proof systems for hybrid logics may induce many redundancies. (...) This paper introduces an internalized tableau system for basic hybrid logic, significantly reducing such redundancies. The calculus enjoys a strong termination property: tableau construction terminates without relying on any specific rule application strategy, and no loop-checking is needed. The treatment of nominal equalities specific of the proposed calculus is briefly compared to other approaches. Its practical advantages are demonstrated by empirical results obtained by use of implemented systems. Finally, it is briefly shown how to extend the calculus to include the global and converse modalities. (shrink)

In an Internet of Things (IoT) environment, IoT devices are typically connected through different network media types such as mobile, wireless and wired networks. Due to the pervasive nature of such devices, they are a potential evidence source in both civil litigation and criminal investigations. It is, however, challenging to identify and acquire forensic artefacts from a broad range of devices, which have varying storage and communication capabilities. Hence, in this paper, we first propose an IoT network architecture for the (...) forensic purpose that uses machine learning algorithms to autonomously detect IoT devices. Then we posit the importance of focusing on the links between different IoT devices (e.g. whether one device is controlled or can be accessed from another device in the system), and design an approach to do so. Specifically, our approach adopts a graph for modelling IoT communications’ message flows to facilitate the identification of correlated network traffic based on the direction of the network and the associated attributes. To demonstrate how such an approach can be deployed in practice, we provide a proof of concept using two IoT controllers to generate 480 commands for controlling two IoT devices in a smart home environment and achieve an accuracy rate of 98.3% for detecting the links between devices. We also evaluate the proposed autonomous discovering of IoT devices and their activities in a TCP network by using real-world measurements from a public dataset of a popular off-the-shelf smart home deployed in two different locations. We selected 39 out of 81 different IoT devices for this evaluation. (shrink)

In recent years, several remarkable results have shown that certain theorems of finite combinatorics are unprovable in certain logical systems. These developments have been instrumental in stimulating research in both areas, with the interface between logic and combinatorics being especially important because of its relation to crucial issues in the foundations of mathematics which were raised by the work of Kurt Godel. Because of the diversity of the lines of research that have begun to shed light on these issues, there (...) was a need for a comprehensive overview which would tie the lines together. This volume fills that need by presenting a balanced mixture of high quality expository and research articles that were presented at the August 1985 AMS-IMS-SIAM Joint Summer Research Conference, held at Humboldt State University in Arcata, California.With an introductory survey to put the works into an appropriate context, the collection consists of papers dealing with various aspects of 'unprovable theorems and fast-growing functions'. Among the topics addressed are: ordinal notations, the dynamical systems approach to Ramsey theory, Hindman's finite sums theorem and related ultrafilters, well quasiordering theory, uncountable combinatorics, nonstandard models of set theory, and a length-of-proof analysis of Godel's incompleteness theorem. Many of the articles bring the reader to the frontiers of research in this area, and most assume familiarity with combinatorics and/or mathematical logic only at the senior undergraduate or first-year graduate level. (shrink)

In recent years, while extensive researches on various networks properties have been proposed and accomplished, little has been proposed and done on network robustness and node vulnerability assessment under cascades in directed large-scale online community networks. In essential, an online directed social network is a group-centered and information spread-dominated online platform which is very different from the traditional undirected social network. Some further research studies have indicated that the online social network has high robustness to random removals of nodes but (...) fails to the intentional attacks, particularly to those attacks based on node betweenness or node directed coefficient. To explore on the robustness of directed social network, in this article, we have proposed two novel node centralities of ITG and I M p v. These two new centrality models are designed to capture this cascading effect in directed online social networks. Furthermore, we also propose a new and highly efficient computing method based on iterations for I M p v. Then, with the abundant experiments on the synthetic signed network and real-life networks derived from directed online social media and directed human mobile phone calling network, it has been proved that our ITG and I M p v based on directed social network robustness and node vulnerability assessment method is more accurate, efficient, and faster than several traditional centrality methods such as degree and betweenness. And we also have proposed the solid reasoning and proof process of iteration times k in computation of I M p v. To the best knowledge of us, our research has drawn some new light on the leading edge of robustness on the directed social network. (shrink)

The notion of efficient proof-checking has always been central to complexity theory, and it gave rise to the definition of the class NP. In the last 15 years there has been a number of exciting, unexpected and deep developments in complexity theory that exploited the notion of randomized and interactive proof-checking. Results developed along this line of research have diverse and powerful applications in complexity theory, cryptography, and the theory of approximation algorithms for combinatorial optimization problems. In this paper we (...) survey the main lines of developments in interactive and probabilistic proof-checking, with an emphasis on open questions. (shrink)

We study from the proof complexity perspective the proof search problem : •Is there an optimal way to search for propositional proofs?We note that, as a consequence of Levin’s universal search, for any fixed proof system there exists a time-optimal proof search algorithm. Using classical proof complexity results about reflection principles we prove that a time-optimal proof search algorithm exists without restricting proof systems iff a p-optimal proof system exists.To characterize precisely the time proof search algorithms need for individual (...) formulas we introduce a new proof complexity measure based on algorithmic information concepts. In particular, to a proof system P we attach information-efficiency function $i_P$ assigning to a tautology a natural number, and we show that: • $i_P$ characterizes time any P-proof search algorithm has to use on $\tau $,•for a fixed P there is such an information-optimal algorithm,•a proof system is information-efficiency optimal iff it is p-optimal,•for non-automatizable systems P there are formulas $\tau $ with short proofs but having large information measure $i_P$.We isolate and motivate the problem to establish unconditional super-logarithmic lower bounds for $i_P$ where no super-polynomial size lower bounds are known. We also point out connections of the new measure with some topics in proof complexity other than proof search. (shrink)

We present logic programming style “goal-directed” proof methods for Łukasiewicz logic Ł that both have a logical interpretation, and provide a suitable basis for implementation. We introduce a basic version, similar to goal-directed calculi for other logics, and make refinements to improve efficiency and obtain termination. We then provide an algorithm for fuzzy logic programming in Rational Pavelka logic RPL, an extension of Ł with rational constants.

Some commentators have worried that Descartes‘s ontological proof is a kind ofafterthought, redundancy, or even embarrassment. Descartes has everythingneeded to establish God as the ground of certainty by Meditation Three, so whybother with yet another proof in Meditation Five? Some have even gone so far asto doubt his sincerity.1Past literature on this topic is of daunting variety andmagnitude, dating back to the seventeenth century.2The current discussion hasfocused on Descartes‘s premises in relation to the coherence of his concept ofGod.3I wish to (...) take up this issue from a somewhat different tack, showing that Descartes‘s ontological proof actually involves a subtle change in the direction ofhis argument from a reflective to a recollective theory of innateness. In the FifthMeditation, Descartes does not simply expand on his previous discussion of God,which arose out of reflection on his self; rather, the ontological proof depends ona kind of recollection of God‘s being that could only be based on the causalpositivity, or ―power,‖ of His existence. God is the structural cause of our idea ofhim and thereby restricts the way in which we may think of Him, in the sameway as the essence of a triangle structurally determines the ways we must thinkof it.4We are not free to construct such ideas in any way we want, so there mustbe a cause, or a reason, that restricts such construction.The specific argument of Meditation Five, however, must be understoodin its larger context, for part of the structurally determined idea of God containsnecessary existence, which Descartes interprets in terms of causal power. In theprocess of explaining this causal power, first to Caterus and, later to Arnauld,Descartes develops a way of interpreting God‘s causal relationship to himself, interms of a scholastic distinction between God as causa sui and ens a se, whichpreserves the universality of the causal principle and allows us to understand whyGod can be considered as the formal cause of His own being—the self-groundingground of all existence—an idea of subsequent importance to Malebranche andSpinoza, among others. Understanding this position on God and cause allows usto see a complementarity between Mediations III and V that has previously beenoverlooked.5While the principle of eminent causality found in Meditation Threeis central to the structural causation argument of Meditation Five, it is God‘spower, the positivity of His causal relationship to himself, that allows theargument from his effects to his existence in the first place.The dualistic structure to Descartes‘s arguments for God‘s existence inMeditations Three and Five mirrors Anselm‘s approach in the Monologion andthe Proslogion. Appreciating this stylistic debt is crucial for understandingDescartes‘s attempts to improve on Anselm‘s arguments, as well as his attempt totruly ground all knowledge in the certainty of God‘s existence. Yet whileAnselm‘s dual argument is ultimately based on a negative intuition of God‘sbeing, described in the Monologion as that without which the world cannot be,Descartes‘s dual argument in Meditations Three and Five is based on a positiveintuition or recollection of God‘s being as a necessary structural restriction on our concepts of the world. The ontological proof is primarily based on thisrecollective theory of innateness. It is God as causa sui, recollected as thenecessary ground of all things, that is the sole efficient cause of the existence ofevery finite, limited thing—especially human beings and their clear and distinctideas. (shrink)

This work studies the structure of proofs containing non-analytic cuts in the cut-based system, a sequent inference system in which the cut rule is not eliminable and the only branching rule is the cut. Such sequent system is invertible, leading to the KE-tableau decision method. We study the structure of such proofs, proving the existence of a normal form for them in the form of a comb-tree proof. We then concentrate on the problem of efficiently computing non-analytic cuts. (...) For that, we study the generalisation of techniques present in many modern theorem provers, namely the techniques of conflict-driven formula learning. (shrink)

This work presents a computational interpretation of the construction process for cyclic linear logic and non-commutative logic sequential proofs. We assume a proof construction paradigm, based on a normalisation procedure known as focussing, which efficiently manages the non-determinism of the construction. Similarly to the commutative case, a new formulation of focussing for NL is used to introduce a general constraint-based technique in order to dealwith partial information during proof construction. In particular, the procedure develops through construction steps propagating constraints (...) in intermediate objects called abstract proofs. (shrink)

The burden of proof (BOP) fallacy is an informal fallacy involving the failure to recognize or properly assign the BOP in a persuasive reasoned dialogue, that is, an interchange between two or more parties whose aim is to prove or defend a position and, in doing so, persuade the other side of its truth or plausibility. In some such dialogues, the amount or strength of evidence required in order to accomplish this goal reasonably may differ for one of the parties (...) involved. The BOP fallacy can occur in two ways. The first is when one side of the dialogue fails to recognize that its opponent incurs the BOP. The second way the BOP fallacy can occur is when one side of the dialogue assigns the BOP incorrectly. There are still some factors that play a role in determining which side of a dialogue incurs the BOP and this chapter discusses these factors. (shrink)

This short sketch of Gödel’s incompleteness proof shows how it arises naturally from Cantor’s diagonalization method [1891]. It renders the proof of the so–called fixed point theorem transparent. We also point out various historical details and make some observations on circularity and some comparisons with natural language. The sketch does not include the messy details of the arithmetization of the language, but the motive for arithmetization and what it should accomplish are made obvious. We suggest this as a way to (...) teach the incompleteness results to students that have had a basic course in logic, which is more efficient than the standard textbooks. For the sake of self–containment Cantor’s original diagonalization is included. A broader and more technical perspective on diagonalization is given in [Gaifman 2005]. Motivated partly by didactic considerations, the present paper presents things somewhat differently. It also includes various points concerning natural language and circularity that appear only here. (shrink)

Who carries the burden of proof in analytic philosophical debates, and how can this burden be satisfied? As it turns out, the answer to this joint question yields a fundamental challenge to the very conduct of metaphysics in analytic philosophy. Empirical research presented in this book indicates that the vastly predominant goal pursued in analytic philosophical dialogues lies not in discovering truths or generating knowledge, but merely in prevailing over one’s opponents. Given this goal, the book examines how most effectively (...) to allocate and discharge the burden of proof. It focuses on premises that must prudently be avoided because a burden of proof on them could never be satisfied, and in particular discusses unsupportable bridge premises across inference barriers, like Hume’s barrier between ‘is’ and ‘ought’, or the barrier between the content of our talk or thought, and the world beyond such content. Employing this content/world barrier for a critical assessment of mainstream analytic philosophical methods, this book argues that we must prudently avoid invoking intuitions or other content of thought or talk in support of claims about the world beyond content, that is, metaphysically significant claims. Yet as content-located evidence is practically indispensable to metaphysical debates throughout analytic philosophy, from ethics to the philosophy of mathematics, this book reaches the startling conclusion that all such metaphysical debates must, prudently, be terminated. (shrink)

The quantum efficiency (QE) of light-induced metastable defect creation in hydrogenated amorphous silicon (a-Si : H) and amorphous As2Se3 (a-As2Se3) by bandgap and subgap illumination has been deduced from photocurrent measurements. The QE decreases with increasing number of absorbed photons. A higher QE for a-As2Se3 than for a-Si : H has been observed and this is interpreted in terms of the higher structural flexibility of a-As2Se3. We have also found that, for both materials, subgap illumination yields a higher QE (...) than does bandgap illumination. (shrink)

If proofs are nothing more than truth makers, then there is no force in the standard argument against classical logic (there is no guarantee that there is either a proof forA or a proof fornot A). The standard intuitionistic conception of a mathematical proof is stronger: there are epistemic constraints on proofs. But the idea that proofs must be recognizable as such by us, with our actual capacities, is incompatible with the standard intuitionistic explanations of the meanings (...) of the logical constants. Proofs are to be recognizable in principle, not necessarily in practice, as shown in section 1. Section 2 considers unknowable propositions of the kind involved in Fitch''s paradox:p and it will never be known thatp. It is argued that the intuitionist faces a dilemma: give up strongly entrenched common sense intuitions about such unknowable propositions, or give up verificationism. The third section considers one attempt to save intuitionism while partly giving up verificationism: keep the idea that a proposition is true iff there is a proof (verification) of it, and reject the idea that proofs must be recognizable in principle. It is argued that this move will have the effect that some standard reasons against classical semantics will be effective also against intuitionism. This is the case with Dummett''s meaning theoretical argument. At the same time the basic reason for regarding proofs as more than mere truth makers is lost. (shrink)

How is the burden of proof to be distributed among individuals who are involved in resolving a particular issue? Under what conditions should the burden of proof be distributed unevenly? We distinguish attitudinal from dialectical burdens and argue that these questions should be answered differently, depending on which is in play. One has an attitudinal burden with respect to some proposition when one is required to possess sufficient evidence for it. One has a dialectical burden with respect to some proposition (...) when one is required to provide supporting arguments for it as part of a deliberative process. We show that the attitudinal burden with respect to certain propositions is unevenly distributed in some deliberative contexts, but in all of these contexts, establishing the degree of support for the proposition is merely a means to some other deliberative end, such as action guidance, or persuasion. By contrast, uneven distributions of the dialectical burden regularly further the aims of deliberation, even in contexts where the quest for truth is the sole deliberative aim, rather than merely a means to some different deliberative end. We argue that our distinction between these two burdens resolves puzzles about unevenness that have been raised in the literature. (shrink)

Nowadays, innovation and entrepreneurship courses occupy a very important place in universities and colleges and have also become an important teaching position in the process of building a new science. Colleges and universities actively respond to the challenge of “mass entrepreneurship and innovation” and define the goals and specifications of the talent training mechanism based on data fusion algorithms to cultivate as much high-quality applied talent as possible. In view of some shortcomings and problems in the current talent training mechanism (...) in universities and colleges, this paper proposes a data fusion algorithm based on information fusion theory and proof theory. The aim is to verify the feasibility of establishing a talent training mechanism for innovation and entrepreneurship education in universities and colleges. And this paper analyzes and explores the data fusion algorithm and the elements of innovation and entrepreneurial talent training, and forms an operating mechanism for entrepreneurial talent training according to social needs. Among them, the efficiency of the data fusion algorithm used by the GM model plays a significant role in the final result, and the minimum relative error value is 3.2%. Finally, it is concluded that we should focus on establishing a perfect talent training system for college students’ innovation and entrepreneurship education to improve students’ own comprehensive quality and various abilities, and to solve some social problems that are difficult to find employment in essence. (shrink)

The study aims to identify the efficiency of the university education performance from the perspective of postgraduate and undergraduate students in international and Palestinian universities. The analytical descriptive approach was used for this purpose and the questionnaire was used as a main tool for data collection. The study community consists of: post graduate students, (23850) graduate students and (146355) undergraduate students. The sample of the study was 378 graduate students and 383 undergraduate students. The random stratified sample was used. (...) The Statistical Package of Social Sciences (SPSS) was also used for data analysis. The study reached a number of results, the most important of which are: The level of efficiency of educational performance in Palestinian and international universities from the point of view of postgraduate and undergraduate students was high. And that there are significant differences between the average views of the sample of the study on the efficiency of educational performance in Palestinian and international universities attributed to the University and to the benefit of international universities. The study concluded many recommendations, the most important of which is the necessity of continuing to develop e-learning strategies that affect the efficiency of educational performance and research commensurate with the university's position in the local and international community, which puts it on the best classification between local and international universities through e-learning. (shrink)