This paper presents an algorithm that, given a finite set E of pairs of second-order monadic terms, returns a finite set U of ‘substitution schemata’ such that a substitution unifies E iff it is an instance of some member of U . Moreover, E is unifiable precisely if U is not empty. The algorithm terminates on all inputs, unlike the unification algorithms for second-order monadic terms developed by G. Huet and G. Winterstein. The substitution schemata in U use (...) expressions which represent sets of terms that differ only in how many times designated strings of function constants follow themselves. The substitution schemata may contain unresolved ‘identity restrictions’; consequently, the members of U generally do not characterize all the unifiers of E in a completely explicit way. The algorithm is particularly useful for investigating the complexity of formal proofs. (shrink)

We study unification problem and problem of admissibility for inference rules in minimal Johanssonsʼ logic J and positive intuitionistic logic IPC+. This paper proves that the problem of admissibility for inference rules with coefficients is decidable for the paraconsistent minimal Johanssonsʼ logic J and the positive intuitionistic logic IPC+. Using obtained technique we show also that the unification problem for these logics is also decidable: we offer algorithms which compute complete sets of unifiers for any unifiable formula. (...) Checking just unifiability of formulas with coefficients also works via verification of admissibility. (shrink)

We propose related algorithms for unification and constraint simplification in }F’&, a refinement of the simply-typed A-calculus with subtypes and bounded intersection types. }F""’ is intended as the basis of a logical framework in order to achieve more succinct and declarative axiomatiza-.

A method is described for inducing a type-logical grammar from a sample of bare sentence trees which are annotated by lambda terms, called term-labelled trees . Any type logic from a permitted class of multimodal logics may be specified for use with the procedure, which induces the lexicon of the grammar including the grammatical categories. A first stage of semantic bootstrapping is performed, which induces a general form lexicon from the sample of term-labelled trees using Fulop’s (J Log Lang Inf (...) 14(1):49–86, 2005) procedure. Next we present a two-stage procedure for performing distributional learning by unifying the lexical types that are initially discovered. The first structural unification algorithm in essence unifies the initial family of sets of types so that the resulting grammar will generate all term-labelled trees that follow the usage patterns evident from the learning sample. Further altering the lexical categories to generate a recursively extended language can be accomplished by a second unification. The combined unification algorithm is shown to yield a new type-logical lexicon that extends the learning sample to a possibly infinite (and possibly context-sensitive) language in a principled fashion. Finally, the complete learning strategy is analyzed from the perspective of algorithmic learning theory; the range of the procedure is shown to be a class of term-labelled tree languages which is finitely learnable from good examples (Lange et al in Algorithmic learning theory, Vol 872 of lecture notes in artificial intelligence, Springer, Berlin, pp 423–437), and so is identifiable in the limit as a corollary. (shrink)

As a result of these restrictions, an implementation of L [subscript lambda] does not need to implement full higher-order unification. Instead, an extension to first-order unification that respects bound variable names and scopes is all that is required. Such unification problems are shown to be decidable and to possess most general unifiers when unifiers exist. A unification algorithm and logic programming interpreter are described and proved correct. Several examples of using L[subscript lambda] as a meta-programming language (...) are presented. (shrink)

We prove that a propositional Linear Temporal Logic with Until and Next has unitary unification. Moreover, for every unifiable in LTL formula A there is a most general projective unifier, corresponding to some projective formula B, such that A is derivable from B in LTL. On the other hand, it can be shown that not every open and unifiable in LTL formula is projective. We also present an algorithm for constructing a most general unifier.

The k-provability for an axiomatic system A is to determine, given an integer k 1 and a formula in the language of A, whether or not there is a proof of in A containing at most k lines. In this paper we develop a unification-theoretic method for investigating the k-provability problem for Parikh systems, which are first-order axiomatic systems that contain a finite number of axiom schemata and a finite number of rules of inference. We show that the k-provability (...) problem for a Parikh system reduces to a unification problem that is essentially the unification problem for second-order terms. By solving various subproblems of this unification problem , we solve the k- probability problem for a variety of Parikh systems, including several formulations of Peano arithmetic. Our method for investigating the k-provability problem employs algorithms that compute and characterize unifiers. We give some examples of how these algorithms can be used to solve complexity problems other than the k-provability problem. (shrink)

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)

We provide an algorithm for determining a categorial grammar from linguistic data that essentially uses unification of type-schemes assigned to atoms. The algorithm presented here extends an earlier one restricted to rigid categorial grammars, introduced in [4] and [5], by admitting non-rigid outputs. The key innovation is the notion of an optimal unifier, a natural generalization of that of a most general unifier.

In this paper we prove some results about the complexity of proofs. We consider proofs in Hilbert-style formal systems such as in [17]. Thus a proof is a sequence offormulas satisfying certain conditions. We can view the formulas as being strings of symbols; hence the whole proof is a string too. We consider the following measures of complexity of proofs: length , depth and number of steps For a particular formal system and a given formula A we consider the shortest (...) length of a proof of A , the minimal depth of a proof of A and the minimal number of steps in a proof of A . The main results are the following: a bound on the depth in terms of the number of steps: Theorem 2.2, a bound on the depth in terms of the length: Theorem 2.3, a bound on the length in terms of the number of steps for restricted systems: Theorem 3.1. These results are applied to obtain several corollaries. In particular we show: a bound on the number of steps in a cut-free proof, some speed-up results, bounds on the number of steps in proofs of Paris-Harrington sentences. Some papers related to our research are listed in the references. We were especially influenced by Parikh's paper [17] on the famous conjecture of Kreisel . Many important problems in this field remain open. We hope that our paper will contribute to progress in this area. It should be noted that some results of this paper can be equally well obtained using unification theory , by translating a complexity-of-proof problem into a unification problem. A unification algorithm solving the unification problem can then be constructed and the complexity of the unification algorithm analyzed. As pointed out by the referee this method can be used to solve the problem stated in Section 3 for some non-simple schematic systems. (shrink)

Instantiation Theory presents a new, general unification algorithm that is of immediate use in building theorem provers and logic programming systems. Instantiation theory is the study of instantiation in an abstract context that is applicable to most commonly studied logical formalisms. The volume begins with a survey of general approaches to the study of instantiation, as found in tree systems, order-sorted algebras, algebraic theories, composita, and instantiation systems. A classification of instantiation systems is given, based on properties of substitutions, (...) degree of type strictness, and well-foundedness of terms. Equational theories and the use of typed variables are studied in terms of quotient homomorphisms and embeddings, respectively. Every instantiation system is a quotient system of a subsystem of first-order term instantiation. The general unification algorithm is developed as an application of the basic theory. Its soundness is rigorously proved, and its completeness and efficiency are verfied for certain classes of instantiation systems. Appropriate applications of the algorithm include unification of first-order terms, order-sorted terms, and first-order formulas modulo alpha-conversion, as well as equational unification using simple congruences. (shrink)

In this paper we prove some results about the complexity of proofs. We consider proofs in Hilbert-style formal systems such as in [17]. Thus a proof is a sequence offormulas satisfying certain conditions. We can view the formulas as being strings of symbols; hence the whole proof is a string too. We consider the following measures of complexity of proofs: length , depth and number of steps For a particular formal system and a given formula A we consider the shortest (...) length of a proof of A , the minimal depth of a proof of A and the minimal number of steps in a proof of A . The main results are the following: a bound on the depth in terms of the number of steps: Theorem 2.2, a bound on the depth in terms of the length: Theorem 2.3, a bound on the length in terms of the number of steps for restricted systems: Theorem 3.1. These results are applied to obtain several corollaries. In particular we show: a bound on the number of steps in a cut-free proof, some speed-up results, bounds on the number of steps in proofs of Paris-Harrington sentences. Some papers related to our research are listed in the references. We were especially influenced by Parikh's paper [17] on the famous conjecture of Kreisel . Many important problems in this field remain open. We hope that our paper will contribute to progress in this area. It should be noted that some results of this paper can be equally well obtained using unification theory , by translating a complexity-of-proof problem into a unification problem. A unification algorithm solving the unification problem can then be constructed and the complexity of the unification algorithm analyzed. As pointed out by the referee this method can be used to solve the problem stated in Section 3 for some non-simple schematic systems. (shrink)

We give some lectures on the work on formal logic of Jacques Herbrand, and sketch his life and his influence on automated theorem proving. The intended audience ranges from students interested in logic over historians to logicians. Besides the well-known correction of Herbrand’s False Lemma by Goedel and Dreben, we also present the hardly known unpublished correction of Heijenoort and its consequences on Herbrand’s Modus Ponens Elimination. Besides Herbrand’s Fundamental Theorem and its relation to the Loewenheim-Skolem-Theorem, we carefully investigate Herbrand’s (...) notion of intuitionism in connection with his notion of falsehood in an infinite domain. We sketch Herbrand’s two proofs of the consistency of arithmetic and his notion of a recursive function, and last but not least, present the correct original text of his unification algorithm with a new translation. (shrink)

We study the decidability of k-provability in \—the relation ‘being provable in \ with at most k steps’—and the decidability of the proof-skeleton problem—the problem of deciding if a given formula has a proof that has a given skeleton. The decidability of k-provability for the usual Hilbert-style formalisation of \ is still an open problem, but it is known that the proof-skeleton problem is undecidable for that theory. Using new methods, we present a characterisation of some numbers k for which (...) k-provability is decidable, and we present a characterisation of some proof-skeletons for which one can decide whether a formula has a proof whose skeleton is the considered one. These characterisations are natural and parameterised by unification algorithms. (shrink)

This paper describes a decision procedure for disjunctions of conjunctions of anti-prenex normal forms of pure first-order logic (FOLDNFs) that do not contain V within the scope of quantifiers. The disjuncts of these FOLDNFs are equivalent to prenex normal forms whose quantifier-free parts are conjunctions of atomic and negated atomic formulae (= Herbrand formulae). In contrast to the usual algorithms for Herbrand formulae, neither skolemization nor unification algorithms with function symbols are applied. Instead, a procedure is described (...) that rests on nothing but equivalence transformations within pure first-order logic (FOL). This procedure involves the application of a calculus for negative normal forms (the NNF-calculus) with A -||- A & A (= &I) as the sole rule that increases the complexity of given FOLDNFs. The described algorithm illustrates how, in the case of Herbrand formulae, decision problems can be solved through a systematic search for proofs that reduce the number of applications of the rule &I to a minimum in the NNF-calculus. In the case of Herbrand formulae, it is even possible to entirely abstain from applying &I. Finally, it is shown how the described procedure can be used within an optimized general search for proofs of contradiction and what kind of questions arise for a &I-minimal proof strategy in the case of a general search for proofs of contradiction. (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)

Quine has argued that modal logic began with the sin of confusing use and mention. Anderson and Belnap, on the other hand, have offered us a way out through a strategy of nominahzation. This paper reviews the history of Lewis's early work in modal logic, and then proves some results about the system in which "A is necessary" is intepreted as "A is a classical tautology.".

This paper offers a brief analysis of the unification problem in modal transitive logics related to the logic S4 : S4 itself, K4, Grz and Gödel-Löb provability logic GL . As a result, new, but not the first, algorithms for the construction of ‘best’ unifiers in these logics are being proposed. The proposed algorithms are based on our earlier approach to solve in an algorithmic way the admissibility problem of inference rules for S4 and Grz . The (...) first algorithms for the construction of ‘best’ unifiers in the above mentioned logics have been given by S. Ghilardi in [ 16 ]. Both the algorithms in [ 16 ] and ours are not much computationally efficient. They have, however, an obvious significant theoretical value a portion of which seems to be the fact that they stem from two different methodological approaches. (shrink)

Proponents of the predictive processing (PP) framework often claim that one of the framework’s significant virtues is its unificatory power. What is supposedly unified are predictive processes in the mind, and these are explained in virtue of a common prediction error-minimisation (PEM) schema. In this paper, I argue against the claim that PP currently converges towards a unified explanation of cognitive processes. Although the notion of PEM systematically relates a set of posits such as ‘efficiency’ and ‘hierarchical coding’ into a (...) unified conceptual schema, neither the frameworks’ algorithmic specifications nor its hypotheses about their implementations in the brain are clearly unified. I propose a novel way to understand the fruitfulness of the research program in light of a set of research heuristics that are partly shared with those common to Bayesian reverse engineering. An interesting consequence of this proposal is that pluralism is at least as important as unification to promote the positive development of the predictive mind. (shrink)

We consider various concepts associated with the revision theory of truth of Gupta and Belnap. We categorize the notions definable using their theory of circular definitions as those notions universally definable over the next stable set. We give a simplified account of varied revision sequences-as a generalised algorithmic theory of truth. This enables something of a unification with the Kripkean theory of truth using supervaluation schemes.

The modeling of the human mind based on quantum effects has been gaining considerable interest due to the intriguing possibility of applying non-local interactions in the studies of consciousness. Inasmuch as the majority of the pertinent studies are restricted to the exclusive analysis of mental phenomena, the quantum model of mind proposed by Roger Penrose constitutes a part of a much larger scheme of the ultimate unification of physics. Penrose's efforts to find the 'missing science of consciousness' presuppose the (...) non-algorithmic character of human thinking inferred from Gödel's incompleteness theorem. This is supposed to combine with the anticipated non-algorithmic character of the future quantum gravity theory involving the objective reduction of a quantum mechanical state vector. By surveying contemporary achievements of cognitive sciences as well as the development of Penrose's conjectures, presented in his recent work The Road to Reality, we wish to show that his non-algorithmic quantum model of human mind is contingent upon the fundamental philosophical assumption of the mathematicity of the Universe. (shrink)

This paper deals with the semantics of de dicto , de re and de se belief reports. First, I flesh out in some detail the established, classical theories that assume syntactic distinctions between all three types of reports. I then propose a new, unified analysis, based on two ideas discarded by the classical theory. These are: (i) modeling the de re/de dicto distinction as a difference in scope, and (ii) analyzing de se as merely a special case of relational de (...) re attitudes. The resurrection of these ideas takes place in a dynamic setting. My formalization of the first idea involves a modification of the presupposition-as-anaphora resolution algorithm for DRT. The second involves treating acquaintance relations as second-order presuppositions, to be bound in the context by means of higher-order unification, or accommodated if necessary. The resulting framework requires no syntactic distinctions between different modes of attitude, with the exception of a specific subclass of de se reports characterized by special ‘ de se pronouns’ (i.e. PRO and logophors). These special pronouns are handled in syntax; everything alse is passed on to the pragmatic resolution module as it appears on the surface. The more sophisticated contextual resolution process nonetheless ensures adequate output truth conditions for a variety of classical and novel puzzles. In particular, I compare the new pragmasemantic system to the classical, syntactic analysis with respect to iterated and quantified reports, and monstrously shifted indexicals. (shrink)

The prominence of Bayesian modeling of cognition has increased recently largely because of mathematical advances in specifying and deriving predictions from complex probabilistic models. Much of this research aims to demonstrate that cognitive behavior can be explained from rational principles alone, without recourse to psychological or neurological processes and representations. We note commonalities between this rational approach and other movements in psychology – namely, Behaviorism and evolutionary psychology – that set aside mechanistic explanations or make use of optimality assumptions. Through (...) these comparisons, we identify a number of challenges that limit the rational program's potential contribution to psychological theory. Specifically, rational Bayesian models are significantly unconstrained, both because they are uninformed by a wide range of process-level data and because their assumptions about the environment are generally not grounded in empirical measurement. The psychological implications of most Bayesian models are also unclear. Bayesian inference itself is conceptually trivial, but strong assumptions are often embedded in the hypothesis sets and the approximation algorithms used to derive model predictions, without a clear delineation between psychological commitments and implementational details. Comparing multiple Bayesian models of the same task is rare, as is the realization that many Bayesian models recapitulate existing (mechanistic level) theories. Despite the expressive power of current Bayesian models, we argue they must be developed in conjunction with mechanistic considerations to offer substantive explanations of cognition. We lay out several means for such an integration, which take into account the representations on which Bayesian inference operates, as well as the algorithms and heuristics that carry it out. We argue this unification will better facilitate lasting contributions to psychological theory, avoiding the pitfalls that have plagued previous theoretical movements. (shrink)

Of all the sub-disciplines of philosophy, the philosophy of science has perhaps the most privileged relationship to information theory. This relationship has been forged through a common interest in themes like induction, probability, confirmation, simplicity, non-ad hocness, unification and, more generally, ontology. It also has historical roots. One of the founders of algorithmic information theory, Ray Solomonoff, produced his seminal work on inductive inference as a direct result of grappling with problems first encountered as a student of the influential (...) philosopher of science Rudolf Carnap. There are other such historical connections between the two fields. Alas, there is no space to explore them here. Instead this essay will restrict its attention to a broad and accessible overview of the aforementioned common themes, which, given their nature, mandate an emphasis on AIT as opposed to general information theory. (shrink)

Electronics can be defined as electromagnetic technology dealing with information, and meta-electronics as a field encompassing all the synergistic technologies in which electronics plays a dominant role. Examining the broad field corresponding to this definition we realize that its history starts some seventy years earlier than the customarily accepted birth of electronics, and, what is more significant, that electronics undergoes a true evolution. This new evolution creates rich, diverse structures similar to those created by the biological evolution. Like biology, electronics (...) is non-teleological, which allows for its unlimited evolutionary development. We propose electronic analogies of all essential biological categories, at all levels: population, speciation, common ancestor, phenotype, extended phenotype, co-evolution, convergent evolution, evolutionary arms race, extinction and mass extinction, hierarchical levels, generative entrenchment, genes, alleles, genome, genetic pool, recombination, mutation, genetic drift, lateral gene transfer, etc. The evolutionary algorithm operating in electronics, like a Darwinian one, includes variation within a population of device models, heredity, natural selection, and a form of selection based on aesthetics and fashion which resembles sexual selection. Algorithm is especially similar to artificial selection, thus possessing directionality in the variational part. Electronic development is orders of magnitude faster than biological, accelerated by that directionality and by other distinct, identifiable mechanisms. Speciation in electronics, as in biology, is best represented on a phylogenetic tree, which starts from a common ancestor, but lately exhibits a unification trend. If continued, this trend may lead to the appearance of a common descendant absent in biology. Our analysis may explain emerging anti-social aspects of electronics and our conclusions add new urgency to recent concerns with unchecked development of Artificial Intelligence. (shrink)

Complex frameworks for defining programming languages aim to generate various tools (e.g. interpreters, symbolic execution engines, deductive verifiers, etc.) using only the formal definition of a language. When used at an industrial scale, these tools are constantly updated, and at the same time, it is required to be trustworthy. Ensuring the correctness of such a framework is practically impossible. A solution is to generate proof objects as correctness artefacts that can be checked by an external trusted checker. A logic suitable (...) for developing such frameworks is matching logic. K framework is a canonical example having matching logic-based foundation. Since the (symbolic) configurations of the programs are represented by matching logic patterns, the algorithms computing the dynamics of these configurations can be seen as pattern transformers and a proof object should be generated for the relationship between these patterns. In this paper, we show that conjunctions and disjunctions of patterns, produced by semantics or analysis rules, can be safely normalized using unification and antiunification algorithms. We also provide a prototype implementation of our proof object generation technique and a checker for certifying the generated objects. (shrink)

The recent move to naturalize phenomenology through a mathematical protocol is a significant advance in consciousness research. It enables a new and fruitful level of dialogue between the cognitive sciences and phenomenology of such a nuanced kind that it also prompts advancement in our phenomenological analyses. But precisely what is going on at this point of ‘dialogue’ between phenomenological descriptions and mathematical algorithms, the latter of which are based on dynamical systems theory? It will be shown that what is (...) happening is something more than a mere ‘passing of the baton’ from phenomenology to mathematics. For this sophisticated naturalization to prove a worthy endeavour it must produce more than just correlation, it must prove some form of interrelation to the extent that phenomenology is deterministic. But such interrelational and deterministic requirements are the start of a slippery slope, and it will be argued that this slope only loses more friction once a further demand of formal and precise descriptions is made of phenomenology. Such deterministic and formally precise demands misconstrue phenomenology’s ideal goal of a unification of genuine/originary reason and truth. Not a deductive and definitive discipline, phenomenology is rather from the outset descriptive and critical. Phenomenology’s descriptive beginnings will thus be employed as an essential barrier to the naturalization of phenomenology. (shrink)

Standpoint logic is a recently proposed formalism in the context of knowledge integration, which advocates a multi-perspective approach permitting reasoning with a selection of diverse and possibly conflicting standpoints rather than forcing their unification. In this paper, we introduce nested sequent calculi for propositional standpoint logics---proof systems that manipulate trees whose nodes are multisets of formulae---and show how to automate standpoint reasoning by means of non-deterministic proof-search algorithms. To obtain worst-case complexity-optimal proof-search, we introduce a novel technique in (...) the context of nested sequents, referred to as "coloring," which consists of taking a formula as input, guessing a certain coloring of its subformulae, and then running proof-search in a nested sequent calculus on the colored input. Our technique lets us decide the validity of standpoint formulae in CoNP since proof-search only produces a partial proof relative to each permitted coloring of the input. We show how all partial proofs can be fused together to construct a complete proof when the input is valid, and how certain partial proofs can be transformed into a counter-model when the input is invalid. These "certificates" (i.e. proofs and counter-models) serve as explanations of the (in)validity of the input. (shrink)

To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit in an ordinary mathematical text, and resolving ambiguities in mathematical expressions. We refer to the process of passing from a quasi-formal and partially-specified expression to a completely precise formal one as elaboration. We describe an elaboration algorithm for dependent type theory that has been implemented in the Lean theorem prover. Lean’s (...) elaborator supports higher-order unification, type class inference, ad hoc overloading, insertion of coercions, the use of tactics, and the computational reduction of terms. The interactions between these components are subtle and complex, and the elaboration algorithm has been carefully designed to balance efficiency and usability. We describe the central design goals, and the means by which they are achieved. (shrink)

_Abstract_: This article discusses the unity of cognitive science that seemed to emerge in the 1950s, based on the computational view of cognition. This unity would entail that there is a single set of mechanisms (i.e. algorithms) for all cognitive behavior, in particular at the level of productive human cognition as exemplified in language and reasoning. In turn, this would imply that theories in psychology, and cognitive science in general, would consist of algorithms based on symbol manipulation as (...) found in digital computing. However, a number of developments in recent decades cast doubt on this unity of cognitive science. Also, there are fundamental problems with the claim that cognitive theories are just algorithms. This article discusses some of these problems and suggests that, instead of unified theories of cognition, specific mechanisms for cognitive behavior in specific cognitive domains could be needed, with architectures that are tailor-made for specific forms of implementation. A sketch of such an architecture for language is presented, based on modifiable connection paths in small-world like network structures. _Keywords_: Connection Paths; Control of Activation; Small-world Networks; Symbol Manipulation; Unity of Cognition _Dalle teoria unificate della cognizione a quelle specifiche_ _Riassunto_: Questo articolo discute l’unità della scienza cognitiva che sembrava emergere negli Anni ’50 e che era basata su una concezione computazionale della cognizione. Questa unità prevedeva l’esistenza di un singolo insieme di meccanismi (algoritmi) per tutti i comportamenti cognitivi, in particolare al livello della cognizione umana produttiva come, per esempio, linguaggio e ragionamento. A sua volta ciò implicava che le teorie psicologiche e, più in generale della scienza cognitiva, prevedessero algoritmi basati sulla manipolazione di simboli come nella computazione digitale. E, tuttavia, diversi sviluppi degli ultimi decenni hanno messo in dubbio questa unità della scienza cognitiva. Affermare che le teorie cognitive sarebbero solo algoritmi presenta problemi di fondo. Questo articolo discute alcuni di questi problemi, suggerendo che, invece di teorie della cognizione unificata, si potrebbe aver bisogno di meccanismi specifici per il comportamento cognitivo in specifici domini cognitivi, con architetture ritagliate per specifiche forme di implementazione. Questo articolo presenta uno schizzo di una simile architettura per il linguaggio, basata su vie di connessione modificabili in piccoli mondi come le strutture di reti. _Parole chiave_: Vie di connessione; Controllo dell’attivazione; Reti di piccoli mondi; Manipolazione di simboli; Unità della cognizione. (shrink)

We present a method for integrating rippling-based rewriting into matrix-based theorem proving as a means for automating inductive specification proofs. The selection of connections in an inductive matrix proof is guided by symmetries between induction hypothesis and induction conclusion. Unification is extended by decision procedures and a rippling/reverse-rippling heuristic. Conditional substitutions are generated whenever a uniform substitution is impossible. We illustrate the integrated method by discussing several inductive proofs for the integer square root problem as well as the (...) class='Hi'>algorithms extracted from these proofs. (shrink)

Algorithms silently structure our lives. Algorithms can determine whether someone is hired, promoted, offered a loan, or provided housing as well as determine which political ads and news articles consumers see. Yet, the responsibility for algorithms in these important decisions is not clear. This article identifies whether developers have a responsibility for their algorithms later in use, what those firms are responsible for, and the normative grounding for that responsibility. I conceptualize algorithms as value-laden, rather (...) than neutral, in that algorithms create moral consequences, reinforce or undercut ethical principles, and enable or diminish stakeholder rights and dignity. In addition, algorithms are an important actor in ethical decisions and influence the delegation of roles and responsibilities within these decisions. As such, firms should be responsible not only for the value-laden-ness of an algorithm but also for designing who-does-what within the algorithmic decision. As such, firms developing algorithms are accountable for designing how large a role individual will be permitted to take in the subsequent algorithmic decision. Counter to current arguments, I find that if an algorithm is designed to preclude individuals from taking responsibility within a decision, then the designer of the algorithm should be held accountable for the ethical implications of the algorithm in use. (shrink)

In philosophy of mind, zombies are imaginary creatures that are exact physical duplicates of conscious subjects but for whom there is no first-personal experience. Zombies are meant to show that physicalism—the theory that the universe is made up entirely out of physical components—is false. In this paper, I apply the zombie thought experiment to the realm of morality to assess whether moral agency is something independent from sentience. Algorithms, I argue, are a kind of functional moral zombie, such that (...) thinking about the latter can help us better understand and regulate the former. I contend that the main reason why algorithms can be neither autonomous nor accountable is that they lack sentience. Moral zombies and algorithms are incoherent as moral agents because they lack the necessary moral understanding to be morally responsible. To understand what it means to inflict pain on someone, it is necessary to have experiential knowledge of pain. At most, for an algorithm that feels nothing, ‘values’ will be items on a list, possibly prioritised in a certain way according to a number that represents weightiness. But entities that do not feel cannot value, and beings that do not value cannot act for moral reasons. (shrink)

This is the first of two papers that use off-training set (OTS) error to investigate the assumption-free relationship between learning algorithms. This first paper discusses the senses in which there are no a priori distinctions between learning algorithms. (The second paper discusses the senses in which there are such distinctions.) In this first paper it is shown, loosely speaking, that for any two algorithms A and B, there are “as many” targets (or priors over targets) for which (...) A has lower expected OTS error than B as vice versa, for loss functions like zero-one loss. In particular, this is true if A is cross-validation and B is “anti-cross-validation” (choose the learning algorithm with largest cross-validation error). This paper ends with a discussion of the implications of these results for computational learning theory. It is shown that one cannot say: if empirical misclassification rate is low, the Vapnik-Chervonenkis dimension of your generalizer is small, and the training set is large, then with high probability your OTS error is small. Other implications for “membership queries” algorithms and “punting” algorithms are also discussed. (shrink)

There have been many attempts to determine what makes a natural kind real, chief among them is the criterion according to which natural kinds must be mind-independent. But it is difficult to specify this criterion: many supposed natural kinds have an element of mind-dependence. I will argue that the mind-independence criterion is nevertheless a good one, if correctly understood: the mind-independence criterion concerns the unification principles for natural kinds. Unification principles determine how natural kinds unify their properties, and (...) only those natural kinds that have a mind-independent unification principle should be considered real. (shrink)

We introduce a fairness criterion that we call Spanning. Spanning i) is implied by Calibration, ii) retains interesting properties of Calibration that some other ways of relaxing that criterion do not, and iii) unlike Calibration and other prominent ways of weakening it, is consistent with Equalized Odds outside of trivial cases.

Machine learning algorithms may radically improve our ability to diagnose and treat disease. For moral, legal, and scientific reasons, it is essential that doctors and patients be able to understand and explain the predictions of these models. Scalable, customisable, and ethical solutions can be achieved by working together with relevant stakeholders, including patients, data scientists, and policy makers.

This essay introduces this special issue on virtue ethics in relation to military AI. It describes the current situation of military AI ethics as following that of AI ethics in general, caught between consequentialism and deontology. Virtue ethics serves as an alternative that can address some of the weaknesses of these dominant forms of ethics. The essay describes how the articles in the issue exemplify the value of virtue-related approaches for these questions, before ending with thoughts for further research.

Part of understanding the meaning and power of algorithms means asking what new demands they might make of ethical frameworks, and how they might be held accountable to ethical standards. I develop a definition of networked information algorithms as assemblages of institutionally situated code, practices, and norms with the power to create, sustain, and signify relationships among people and data through minimally observable, semiautonomous action. Starting from Merrill’s prompt to see ethics as the study of “what we ought (...) to do,” I examine ethical dimensions of contemporary NIAs. Specifically, in an effort to sketch an empirically grounded, pragmatic ethics of algorithms, I trace an algorithmic assemblage’s power to convene constituents, suggest actions based on perceived similarity and probability, and govern the timing and timeframes of ethical action. (shrink)

This essay asks how we might articulate a political theory of algorithms. To do so, I propose a political ontology of the algorithm dispositif that elaborates how algorithms arrange the movement of energies in space and time, and how they do so automatically. This force of arrangement is what I refer to as the dispositional power of algorithms that I identify as a political physics of vital processes. The essay is divided into three sections. The first provides (...) readers of Political Theory with a discussion of three notable works in the field of critical algorithm studies relevant to a political theory of algorithms. The subsequent sections of the essay elaborate an understanding of the political ontology of the algorithm dispositif by focusing (first) on the difference that a virtual ontology introduces to our political reflections and (second) on the cybernetic operation of negative feedback that I identify as foundational to understanding an algorithm’s political physics of vital processes. I conclude that any political theory engagement with technical media can’t simply rest on an epistemic analysis of the normative effects of media but must also pursue an investigation into a medium’s modes of existence in the world. (shrink)

Multiobjective evolutionary algorithms have witnessed prosperity in solving many-objective optimization problems over the past three decades. Unfortunately, no one single MOEA equipped with given parameter settings, mating-variation operator, and environmental selection mechanism is suitable for obtaining a set of solutions with excellent convergence and diversity for various types of MaOPs. The reality is that different MOEAs show great differences in handling certain types of MaOPs. Aiming at these characteristics, this paper proposes a flexible ensemble framework, namely, ASES, which is (...) highly scalable for embedding any number of MOEAs to promote their advantages. To alleviate the undesirable phenomenon that some promising solutions are discarded during the evolution process, a big archive that number of contained solutions be far larger than population size is integrated into this ensemble framework to record large-scale nondominated solutions, and also an efficient maintenance strategy is developed to update the archive. Furthermore, the knowledge coming from updating archive is exploited to guide the evolutionary process for different MOEAs, allocating limited computational resources for efficient algorithms. A large number of numerical experimental studies demonstrated superior performance of the proposed ASES. Among 52 test instances, the ASES performs better than all the six baseline algorithms on at least half of the test instances with respect to both metrics hypervolume and inverted generational distance. (shrink)