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

There are many algorithm texts that provide lots of well-polished code and proofs of correctness. Instead, this book presents insights, notations, and analogies to help the novice describe and think about algorithms like an expert. By looking at both the big picture and easy step-by-step methods for developing algorithms, the author helps students avoid the common pitfalls. He stresses paradigms such as loop invariants and recursion to unify a huge range of algorithms into a few meta-algorithms. (...) Part of the goal is to teach the students to think abstractly. Without getting bogged with formal proofs, the book fosters a deeper understanding of how and why each algorithm works. These insights are presented in a slow and clear manner accessible to second- or third-year students of computer science, preparing them to find their own innovative ways to solve problems. (shrink)

This book introduces students to the art and craft of writing proofs, beginning with the basics of writing proofs and logic, and continuing on with more in-depth issues and examples of creating proofs in different parts of mathematics, as well as introducing proofs-of-correctness for algorithms. The creation of proofs is covered for theorems in both discrete and continuous mathematics, and in difficulty ranging from elementary to beginning graduate level. Just beyond the standard introductory courses on calculus, theorems and proofs (...) become central to mathematics. Students often find this emphasis difficult and new. This book is a guide to understanding and creating proofs. It explains the standard "moves" in mathematical proofs: direct computation, expanding definitions, proof by contradiction, proof by induction, as well as choosing notation and strategies. (shrink)

Suppose that fn is a sequence of nonnegative functions with compact support on a locally compact metric space, that T is a nonnegative linear functional, and that equation imageT fn < T f0. A result of Bishop, foundational to a constructive theory of functional analysis, asserts the existence of a point x such that equation imagefn < f0. This paper extends this result to arbitrary Hausdorff spaces, and gives short proofs using nonstandard analysis. While such arguments used are not themselves (...) constructive, they can illuminate where the difficulty lies in finding the point x. An algorithm for constructing x is then given, with a nonstandard proof that the algorithm converges to a correct value. (shrink)

It is argued that the truth status of emergent properties of complex adaptive systems models should be based on an epistemology of proof by constructive verification and therefore on the ontological axioms of a non-realist logical system such as constructivism or intuitionism. ‘Emergent’ properties of complex adaptive systems models create particular epistemological and ontological challenges. These challenges bear directly on current debates in the philosophy of mathematics and in theoretical computer science. CAS research, with its emphasis on computer simulation, (...) is heavily reliant on models which explore the entailments of Formal Axiomatic Systems. The incompleteness results of G¨odel, the incomputability results of Turing, and the Algorithmic Information Theory results of Chaitin, undermine a realist truth model of emergent properties. These same findings support the hegemony of epistemology over ontology and point to alternative truth models such as intuitionism, constructivism and quasi-empiricism. (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)

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)

Machine intelligence already helps medical staff with a number of tasks. Ethical decision-making, however, has not been handed over to computers. In this proof-of-concept study, we show how an algorithm based on Beauchamp and Childress’ prima-facie principles could be employed to advise on a range of moral dilemma situations that occur in medical institutions. We explain why we chose fuzzy cognitive maps to set up the advisory system and how we utilized machine learning to train it. We report on (...) the difficult task of operationalizing the principles of beneficence, non-maleficence and patient autonomy, and describe how we selected suitable input parameters that we extracted from a training dataset of clinical cases. The first performance results are promising, but an algorithmic approach to ethics also comes with several weaknesses and limitations. Should one really entrust the sensitive domain of clinical ethics to machine intelligence? (shrink)

This chapter contains sections titled: The Cutting Edge Automated Reasoning, Principles and Elements Significant Successes Myths, Mechanization, and Mystique.

The problem of algorithmic structuring of proofs in the sequent calculi LK and LKB ( LK where blocks of quantifiers can be introduced in one step) is investigated, where a distinction is made between linear proofs and proofs in tree form. In this framework, structuring coincides with the introduction of cuts into a proof. The algorithmic solvability of this problem can be reduced to the question of k-l-compressibility: "Given a proof of length k , and l ≤ k (...) : Is there is a proof of length ≤ l ?" When restricted to proofs with universal or existential cuts, this problem is shown to be (1) undecidable for linear or tree-like LK-proofs (corresponds to the undecidability of second order unification), (2) undecidable for linear LKB-proofs (corresponds to the undecidability of semi-unification), and (3) decidable for tree-like LKB -proofs (corresponds to a decidable subprob- lem of semi-unification). (shrink)

A new approach to informal rigorous mathematical proof is offered. To this end, algorithmic devices are characterized and their central role in mathematical proof delineated. It is then shown how all the puzzling aspects of mathematical proof, including its peculiar capacity to convince its practitioners, are explained by algorithmic devices. Diagrammatic reasoning is also characterized in terms of algorithmic devices, and the algorithmic device view of mathematical proof is compared to alternative construals of informal proof (...) to show its superiority. (shrink)

In this work we develop goal-directed deduction methods for the implicational fragment of several modal logics. We give sound and complete procedures for strict implication of K, T, K4, S4, K5, K45, KB, KTB, S5, G and for some intuitionistic variants. In order to achieve a uniform and concise presentation, we first develop our methods in the framework of Labelled Deductive Systems [Gabbay 96]. The proof systems we present are strongly analytical and satisfy a basic property of cut admissibility. (...) We then show that for most of the systems under consideration the labelling mechanism can be avoided by choosing an appropriate way of structuring theories. One peculiar feature of our proof systems is the use of restart rules which allow to re-ask the original goal of a deduction. In case of K, K4, S4 and G, we can eliminate such a rule, without loosing completeness. In all the other cases, by dropping such a rule, we get an intuitionistic variant of each system. The present results are part of a larger project of a goal directed proof theory for non-classical logics; the purpose of this project is to show that most implicational logics stem from slight variations of a unique deduction method, and from different ways of structuring theories. Moreover, the proof systems we present follow the logic programming style of deduction and seem promising for proof search [Gabbay and Reyle 84, Miller et al. 91]. (shrink)

The development of mathematics toward greater precision has led, as is well known, to the formalization of large tracts of it, so that one can prove any theorem using nothing but a few mechanical rules. -- Godel [11].

This paper presents a new method - which does not rely on the cut-elimination theorem - for characterizing the provably total functions of certain intuitionistic subsystems of arithmetic. The new method hinges on a realizability argument within an infinitary language. We illustrate the method for the intuitionistic counterpart of Buss's theory Smath image, and we briefly sketch it for the other levels of bounded arithmetic and for the theory IΣ1.

This article features long-sought proofs with intriguing properties (such as the absence of double negation and the avoidance of lemmas that appeared to be indispensable), and it features the automated methods for finding them. The theorems of concern are taken from various areas of logic that include two-valued sentential (or propositional) calculus and infinite-valued sentential calculus. Many of the proofs (in effect) answer questions that had remained open for decades, questions focusing on axiomatic proofs. The approaches we take are (...) of added interest in that all rely heavily on the use of a single program that offers logical reasoning, William McCune's automated reasoning program OTTER. The nature of the successes and approaches suggests that this program offers researchers a valuable automated assistant. This article has three main components. First, in view of the interdisciplinary nature of the audience, we discuss the means for using the program in question (OTTER), which flags, parameters, and lists have which effects, and how the proofs it finds are easily read. Second, because of the variety of proofs that we have found and their significance, we discuss them in a manner that permits comparison with the literature. Among those proofs, we offer a proof shorter than that given by Meredith and Prior in their treatment of ukasiewicz's shortest single axiom for the implicational fragment of two-valued sentential calculus, and we offer a proof for the ukasiewicz 23-letter single axiom for the full calculus. Third, with the intent of producing a fruitful dialogue, we pose questions concerning the properties of proofs and, even more pressing, invite questions similar to those this article answers. (shrink)

We introduce a reciprocity criterion for coalition formation among goal-directed agents, which we call the indecomposable do-ut-des property. It refines an older reciprocity property, called the do-ut-des or give-to-get property by considering the fact that agents prefer to form coalitions whose components cannot be formed independently. A formal description of this property is provided as well as an analysis of algorithms and their complexity. We provide an algorithm to decide whether a coalition has the desired property, and we show (...) that the problem to verify whether a single coalition satisfies the property is tractable. Moreover, we provide an algorithm to search all the sub-coalitions of a given coalition satisfying the new property. Even if this problem is not computationally tractable, we show that in several cases, also the complexity of this problem may decrease considerably. (shrink)

This paper reports on an exploration of Boolos’ Curious Inference, using higher-order automated theorem provers (ATPs). Surprisingly, only suitable shorthand notations had to be provided by hand for ATPs to find a short proof. The higher-order lemmas required for constructing a short proof are automatically discovered by the ATPs. Given the observations and suggestions in this paper, full proof automation of Boolos’ and related examples now seems to be within reach of higher-order ATPs.

In 2004 Atserias, Kolaitis, and Vardi proposed $\text {OBDD}$ -based propositional proof systems that prove unsatisfiability of a CNF formula by deduction of an identically false $\text {OBDD}$ from $\text {OBDD}$ s representing clauses of the initial formula. All $\text {OBDD}$ s in such proofs have the same order of variables. We initiate the study of $\text {OBDD}$ based proof systems that additionally contain a rule that allows changing the order in $\text {OBDD}$ s. At first we consider (...) a proof system $\text {OBDD}$ that uses the conjunction rule and the rule that allows changing the order. We exponentially separate this proof system from $\text {OBDD}$ proof system that uses only the conjunction rule. We prove exponential lower bounds on the size of $\text {OBDD}$ refutations of Tseitin formulas and the pigeonhole principle. The first lower bound was previously unknown even for $\text {OBDD}$ proofs and the second one extends the result of Tveretina et al. from $\text {OBDD}$ to $\text {OBDD}$.In 2001 Aguirre and Vardi proposed an approach to the propositional satisfiability problem based on $\text {OBDD}$ s and symbolic quantifier elimination $ algorithms). We augment these algorithms with the operation of reordering of variables and call the new scheme $\text {OBDD}$ algorithms. We notice that there exists an $\text {OBDD}$ algorithm that solves satisfiable and unsatisfiable Tseitin formulas in polynomial time, but we show that there are formulas representing systems of linear equations over $\mathbb {F}_2$ that are hard for $\text {OBDD}$ algorithms. Our hard instances are satisfiable formulas representing systems of linear equations over $\mathbb {F}_2$ that correspond to checksum matrices of error correcting codes. (shrink)

In this book, we present a study of linear models and algorithms to find the optimal solution for them using the concepts of neuroscientific science. We know that the linear programming method is one of the important methods of operations research, the science that was the product of the great scientific development that our contemporary world is witnessing. The name operations research is given to the group of scientific methods used. In analyzing problems and searching for optimal solutions, it (...) is a science whose applications have achieved widespread success in various fields of life. What is meant by neutrosophic models are models in which the data are neutrosophic values, that is, variables such as in the objective function, which expresses profit if the model is a maximization model, and expresses a cost if the model is a minimization model, which in turn is affected by environmental conditions. (shrink)

Apologies. The purpose of the following talk is to give an overview of the present state of aims, methods and results in Pure Proof Theory. Shortage of time forces me to concentrate on my very personal views. This entails that I will emphasize the work which I know best, i.e., work that has been done in the triangle Stanford, Munich and Münster. I am of course well aware that there are as important results coming from outside this triangle and (...) I apologize for not displaying these results as well.Moreover the audience should be aware that in some points I have to oversimplify matters. Those who complain about that are invited to consult the original papers.1.1. General. Proof theory startedwithHilbert's Programme which aimed at a finitistic consistency proof for mathematics.By Gödel's Theorems, however, we know that we can neither formalize all mathematics nor even prove the consistency of formalized fragments by finitistic means. Inspite of this fact I want to give some reasons why I consider proof theory in the style of Gentzen's work still as an important and exciting field of Mathematical Logic. I will not go into applications of Gentzen's cut-elimination technique to computer science problems—this may be considered as applied proof theory—but want to concentrate on metamathematical problems and results. In this sense I am talking about Pure Proof Theory.Mathematicians are interested in structures. There is only one way to find the theorems of a structure. Start with an axiom system for the structure and deduce the theorems logically. These axiom systems are the objects of proof-theoretical research. Studying axiom systems there is a series of more or less obvious questions. (shrink)

Bilingualism has been identified as a potential cognitive factor linked to delayed onset of dementia as well as boosting executive functions in healthy individuals. However, more recently, this claim has been called into question following several failed replications. It remains unclear whether these contradictory findings reflect how bilingualism is defined between studies, or methodological limitations when measuring the bilingual effect. One key issue is that despite the claims that bilingualism yields general protection to cognitive processes, studies reporting putative bilingual differences (...) are often focused on domain specific experimental paradigms. This study chose a broader approach, by considering the consequences of bilingualism on a wide range of cognitive functions within individuals. We utilised 19 measures of different cognitive functions commonly associated with bilingual effects, to form a “cognitive profile” for 215 non-clinical participants. We recruited Welsh speakers, who as a group of bilinguals were highly homogeneous, as means of isolating the bilingualism criterion. We sought to determine if such analyses would independently classify bilingual/monolingual participant groups based on emergent patterns driven by collected cognitive profiles, such that population differences would emerge. Multiple predictive models were trained to independently recognise the cognitive profiles of bilinguals, older adults and higher education attainment. Despite managing to successfully classify cognitive profiles based on age and education, the model failed to differentiate between bilingual and monolingual cognitive ability at a rate greater than that of chance. Repeated modelling using alternative definitions of bilingualism, and just the older adults, yielded similar results. In all cases then, using our “bottom–up” analytical approach, there was no evidence that bilingualism as a variable indicated differential cognitive performance – as a consequence, we conclude that bilinguals are not cognitively different from their monolingual counterparts, even in older demographics. We suggest that studies that have reported a bilingual advantage could well have confounded other key variables that may be driving reported advantages. We recommend that future research refine the machine learning methods used in this study to further investigate the complex relationship between bilingualism and cognition. (shrink)

We present a study of linear models using the concepts of neutrosophic science, the science that was built on the basis that there is no absolute truth, there is no confirmed data, issues cannot be limited to right and wrong only. There is a third state between error and right, an indeterminate, undetermined, uncertain state. It is indeterminacy. Neutrosophic science gave each issue three dimensions, namely (T, I, F), correctness in degrees, indeterminacy in degrees, and error in degrees. It was (...) founded by the American philosopher and mathematician Florentin Smarandache, in 1995 and came as a generalization of fuzzy logic that was founded by the scientist Lotfi. A. Zadeh, in 1965. (shrink)

Over the previous three decades, the area of computer networks has progressed significantly, from traditional static networks to dynamically designed architecture. The primary purpose of software-defined networking is to create an open, programmable network. Conventional network devices, such as routers and switches, may make routing decisions and forward packets; however, SDN divides these components into the Data plane and the Control plane by splitting distinct features away. As a result, switches can only forward packets and cannot make routing decisions; the (...) controller makes routing decisions. OpenFlow is the communication interface between the switches and the controller. It is a protocol that allows the controller to identify the network packet’s path across the switches. This project uses the SDN environment to implement the firefly optimization algorithm to determine the shortest path between two nodes in a network. The firefly optimization algorithm was implemented using Ryu control. The results reveal that using the firefly optimization algorithm improves the selected short path between the source and destination. (shrink)

Combining physics, mathematics and computer science, quantum computing and its sister discipline of quantum information have developed in the past few decades from visionary ideas to two of the most fascinating areas of quantum theory. General interest and excitement in quantum computing was initially triggered by Peter Shor (1994) who showed how a quantum algorithm could exponentially “speed-up” classical computation and factor large numbers into primes far more efficiently than any (known) classical algorithm. Shor’s algorithm was soon followed by several (...) other algorithms that aimed to solve combinatorial and algebraic problems, and in the years since theoretical study of quantum systems serving as computational devices has achieved tremendous progress. Common belief has it that the implementation of Shor’s algorithm on a large scale quantum computer would have devastating consequences for current cryptography protocols which rely on the premise that all known classical worst-case algorithms for factoring take time exponential in the length of their input (see, e.g., Preskill 2005). Consequently, experimentalists around the world are engaged in attempts to tackle the technological difficulties that prevent the realisation of a large scale quantum computer. But regardless whether these technological problems can be overcome (Unruh 1995; Ekert and Jozsa 1996; Haroche and Raimond 1996), it is noteworthy that no proof exists yet for the general superiority of quantum computers over their classical counterparts. -/- The philosophical interest in quantum computing is manifold. From a social-historical perspective, quantum computing is a domain where experimentalists find themselves ahead of their fellow theorists. Indeed, quantum mysteries such as entanglement and nonlocality were historically considered a philosophical quibble, until physicists discovered that these mysteries might be harnessed to devise new efficient algorithms. But while the technology for harnessing the power of 50–100 qubits (the basic unit of information in the quantum computer) is now within reach (Preskill 2018), only a handful of quantum algorithms exist, and the question of whether these can truly outperform any conceivable classical alternative is still open. From a more philosophical perspective, advances in quantum computing may yield foundational benefits. For example, it may turn out that the technological capabilities that allow us to isolate quantum systems by shielding them from the effects of decoherence for a period of time long enough to manipulate them will also allow us to make progress in some fundamental problems in the foundations of quantum theory itself. Indeed, the development and the implementation of efficient quantum algorithms may help us understand better the border between classical and quantum physics (Cuffaro 2017, 2018a; cf. Pitowsky 1994, 100), and perhaps even illuminate fundamental concepts such as measurement and causality. Finally, the idea that abstract mathematical concepts such as computability and complexity may not only be translated into physics, but also re-written by physics bears directly on the autonomous character of computer science and the status of its theoretical entities—the so-called “computational kinds”. As such it is also relevant to the long-standing philosophical debate on the relationship between mathematics and the physical world. (shrink)

In a recent article published in this journal (van Deemter, Gatt, van der Sluis, & Power, 2012), the authors criticize the Incremental Algorithm (a well-known algorithm for the generation of referring expressions due to Dale & Reiter, 1995, also in this journal) because of its strong reliance on a pre-determined, domain-dependent Preference Order. The authors argue that there are potentially many different Preference Orders that could be considered, while often no evidence is available to determine which is a good one. (...) In this brief note, however, we suggest (based on a learning curve experiment) that finding a Preference Order for a new domain may not be so difficult after all, as long as one has access to a handful of human-produced descriptions collected in a semantically transparent way. We argue that this is due to the fact that it is both more important and less difficult to get a good ordering of the head than of the tail of a Preference Order. (shrink)

Science is the basis for managing the affairs of life and human activities, and living without knowledge is a form of wandering and a kind of loss. Using scientific methods helps us understand the foundations of choice, decision-making, and adopting the right solutions when solutions abound and options are numerous. Operational research is considered the best that scientific development has provided because its methods depend on the application of scientific methods in solving complex issues and the optimal use of available (...) resources in various fields, private and governmental work in peace and war, in politics and economics, in planning and implementation, and in various aspects of life. Its basic essence is to use the data provided for the issue under study to build a mathematical model that is the optimal solution. It is the basis on which decision makers rely in managing institutions and companies, and when operations research methods meet with the neutrosophic teacher, we get ideal solutions that take into account all the circumstances and fluctuations that may occur in the work environment over time. One of the most important operations research methods is the linear programming method. Which prompted us to reformulate the linear models, the graphical method, and the simplex method, which are used to obtain the optimal solution for linear models using the concepts of neutrosophic science. In this research, and as a continuation of what we presented previously, we will reformulate the modified simplex algorithm that was presented to address the difficulty that we were facing when applying the direct simplex algorithm. It is the large number of calculations required to be performed in each step of the solution, which requires a lot of time and effort. (shrink)

Firms use algorithms to make important business decisions. To date, the algorithmic accountability literature has elided a fundamentally empirical question important to business ethics and management: Under what circumstances, if any, are algorithmic decision-making systems considered legitimate? The present study begins to answer this question. Using factorial vignette survey methodology, we explore the impact of decision importance, governance, outcomes, and data inputs on perceptions of the legitimacy of algorithmic decisions made by firms. We find that many of the procedural (...) governance mechanisms in practice today, such as notices and impact statements, do not lead to algorithmic decisions being perceived as more legitimate in general, and, consistent with legitimacy theory, that algorithmic decisions with good outcomes are perceived as more legitimate than bad outcomes. Yet, robust governance, such as offering an appeal process, can create a legitimacy dividend for decisions with bad outcomes. However, when arbitrary or morally dubious factors are used to make decisions, most legitimacy dividends are erased. In other words, companies cannot overcome the legitimacy penalty of using arbitrary or morally dubious factors, such as race or the day of the week, with a good outcome or an appeal process for individuals. These findings add new perspectives to both the literature on legitimacy and policy discussions on algorithmic decision-making in firms. (shrink)

We cooperate with other people despite the risk of being exploited or hurt. If future artificial intelligence (AI) systems are benevolent and cooperative toward us, what will we do in return? Here we show that our cooperative dispositions are weaker when we interact with AI. In nine experiments, humans interacted with either another human or an AI agent in four classic social dilemma economic games and a newly designed game of Reciprocity that we introduce here. Contrary to the hypothesis that (...) people mistrust algorithms, participants trusted their AI partners to be as cooperative as humans. However, they did not return AI's benevolence as much and exploited the AI more than humans. These findings warn that future self-driving cars or co-working robots, whose success depends on humans' returning their cooperativeness, run the risk of being exploited. This vulnerability calls not just for smarter machines but also better human-centered policies. (shrink)

Algorithmic decision-making based on profiling may significantly affect people’s destinies. As a rule, however, explanations for such decisions are lacking. What are the chances for a “right to explanation” to be realized soon? After an exploration of the regulatory efforts that are currently pushing for such a right it is concluded that, at the moment, the GDPR stands out as the main force to be reckoned with. In cases of profiling, data subjects are granted the right to receive meaningful information (...) about the functionality of the system in use; for fully automated profiling decisions even an explanation has to be given. However, the trade secrets and intellectual property rights (IPRs) involved must be respected as well. These conflicting rights must be balanced against each other; what will be the outcome? Looking back to 1995, when a similar kind of balancing had been decreed in Europe concerning the right of access (DPD), Wachter et al. (2017) find that according to judicial opinion only generalities of the algorithm had to be disclosed, not specific details. This hardly augurs well for a future right of access let alone to explanation. Thereupon the landscape of IPRs for machine learning (ML) is analysed. Spurred by new USPTO guidelines that clarify when inventions are eligible to be patented, the number of patent applications in the US related to ML in general, and to “predictive analytics” in particular, has soared since 2010—and Europe has followed. I conjecture that in such a climate of intensified protection of intellectual property, companies may legitimately claim that the more their application combines several ML assets that, in addition, are useful in multiple sectors, the more value is at stake when confronted with a call for explanation by data subjects. Consequently, the right to explanation may be severely crippled. (shrink)

Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame (...) class is found. The method is a synthesis of a generation of calculi with internalized relational semantics, a Tait–Schütte–Takeuti style completeness proof, and procedures to finitize the countermodel construction. Finitizations for intuitionistic propositional logic are obtained through the search for a minimal derivation, through pruning of infinite branches in search trees by means of a suitable syntactic counterpart of semantic filtration, or through a proof-theoretic embedding into an appropriate provability logic. A number of examples illustrates the method, its subtleties, challenges, and present scope. (shrink)

This work provides proof-search algorithms and automated counter-model extraction for a class of STIT logics. With this, we answer an open problem concerning syntactic decision procedures and cut-free calculi for STIT logics. A new class of cut-free complete labelled sequent calculi G3LdmL^m_n, for multi-agent STIT with at most n-many choices, is introduced. We refine the calculi G3LdmL^m_n through the use of propagation rules and demonstrate the admissibility of their structural rules, resulting in auxiliary calculi Ldm^m_nL. In the single-agent (...) case, we show that the refined calculi Ldm^m_nL derive theorems within a restricted class of (forestlike) sequents, allowing us to provide proof-search algorithms that decide single-agent STIT logics. We prove that the proof-search algorithms are correct and terminate. (shrink)

Artificial intelligence plays an increasingly important role in legal disputes, influencing not only the reality outside the court but also the judicial decision-making process itself. While it is clear why judges may generally benefit from technology as a tool for reducing effort costs or increasing accuracy, the presence of technology in the judicial process may also affect the public perception of the courts. In particular, if individuals are averse to adjudication that involves a high degree of automation, particularly given fairness (...) concerns, then judicial technology may yield lower benefits than expected. However, the degree of aversion may well depend on how technology is used, i.e., on the timing and strength of judicial reliance on algorithms. Using an exploratory survey, we investigate whether the stage in which judges turn to algorithms for assistance matters for individual beliefs about the fairness of case outcomes. Specifically, we elicit beliefs about the use of algorithms in four different stages of adjudication: (i) information acquisition, (ii) information analysis, (iii) decision selection, and (iv) decision implementation. Our analysis indicates that individuals generally perceive the use of algorithms as fairer in the information acquisition stage than in other stages. However, individuals with a legal profession also perceive automation in the decision implementation stage as less fair compared to other individuals. Our findings, hence, suggest that individuals do care about how and when algorithms are used in the courts. (shrink)

Big Data evangelists often argue that algorithms make decision-making more informed and objective—a promise hotly contested by critics of these technologies. Yet, to date, most of the debate has focused on the instruments themselves, rather than on how they are used. This article addresses this lack by examining the actual practices surrounding algorithmic technologies. Specifically, drawing on multi-sited ethnographic data, I compare how algorithms are used and interpreted in two institutional contexts with markedly different characteristics: web journalism and (...) criminal justice. I find that there are surprising similarities in how web journalists and legal professionals use algorithms in their work. In both cases, I document a gap between the intended and actual effects of algorithms—a process I analyze as “decoupling.” Second, I identify a gamut of buffering strategies used by both web journalists and legal professionals to minimize the impact of algorithms in their daily work. Those include foot-dragging, gaming, and open critique. Of course, these similarities do not exhaust the differences between the two cases, which are explored in the discussion section. I conclude with a call for further ethnographic work on algorithms in practice as an important empirical check against the dominant rhetoric of algorithmic power. (shrink)

Studying drug relationships can provide deeper information for the construction and maintenance of biomedical databases and provide more important references for disease treatment and drug development. The research model has expanded from the previous focus on a certain drug to the systematic analysis of the pharmaceutical network formed between drugs. Network model is suitable for the study of the nonlinear relationship of the pharmaceutical relationship by modeling the data learning. Association rule mining is used to find the potential correlations between (...) the various sets of massive data. Therefore, based on the network model, this research proposed an algorithm for drug interaction under improved association rules, which achieved accurate analysis and decision-making of drug relationship. Meanwhile, this research applied the established association rule algorithm to discuss the relationship between Chinese medicine and mental illness medicine and conducted the algorithm research and simulation analysis of the association relationship. The results showed the association rule algorithm based on the network model constructed was better than other association algorithms. It had reliability and superiority in decision-making in improving the drug-drug relationship. It also promoted the rational use of medicines and played a guiding role in pharmaceutical research. This provides scientific research personnel with research basis and research ideas for disease-related diagnosis. (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 paper presents a proof-theoretic semantics (PTS) for a fragment of natural language, providing an alternative to the traditional model-theoretic (Montagovian) semantics (MTS), whereby meanings are truth-condition (in arbitrary models). Instead, meanings are taken as derivability-conditions in a dedicated natural-deduction (ND) proof-system. This semantics is effective (algorithmically decidable), adhering to the meaning as use paradigm, not suffering from several of the criticisms formulated by philosophers of language against MTS as a theory of meaning. In particular, Dummett’s manifestation argument (...) does not obtain, and assertions are always warranted, having grounds of assertion. The proof system is shown to satisfy Dummett’s harmony property, justifying the ND rules as meaning conferring. The semantics is suitable for incorporation into computational linguistics grammars, formulated in type-logical grammar. (shrink)

The use of machine learning algorithms has become ubiquitous in hiring decisions. Recent studies have shown that many of these algorithms generate unlawful discriminatory effects in every step of the process. The training phase of the machine learning models used in these decisions has been identified as the main source of bias. For a long time, discrimination cases have been analyzed under the banner of disparate treatment and disparate impact, but these concepts have been shown to be ineffective (...) in the context of AI. This paper examines the possibility of studying algorithmic discrimination from the perspective of negligence law. Negligent selection and validation of datasets and classifiers is a salient cause of improper training in machine learning. It is a breach of an employer’s duty to protect others, a failure of its exercise of due care in the manner of choosing employees. Adopting negligence to algorithmic discrimination requires a reformulation of what is foreseeable and reasonable within the context of black box algorithms, and a shift in the burden of proof to the employer, who must present evidence of its efforts to avoid bias. (shrink)

This paper is about the opposite of judgement and calculation. This opposition has been a traditional anchor of critiques concerned with the rise of AI decision making over human judgement. Contrary to these approaches, it is argued that human judgement is not and cannot be replaced by calculation, but that it is human judgement that contextualises computational structures and gives them meaning and purpose. The article focuses on the epistemic structure of algorithms and artificial neural networks to find that (...) they always depend on human judgement to be related to real life objects or purposes. By introducing the philosophical concept of judgement, it becomes clear that the property of judgement to provide meaning and purposiveness is based on the temporality of human life and the ambiguity of language, which quantitative processes lack. A juxtaposition shows that calculations and clustering can be used and referred to in more or less prejudiced and reflecting as well as opaque and transparent ways, but thereby always depend on human judgement. The paper clearly asserts that the transparency of AI is necessary for their autonomous use. This transparency requires the explicitness of the judgements that constitute these computational structures, thereby creating an awareness of the conditionality of such epistemic entities. (shrink)