The Joint International Conference on Logic Programming, sponsored by the Association for Logic Programming, is a major forum for presentations of research, applications, and implementations in this important area of computer science. Logic programming is one of the most promising steps toward declarative programming and forms the theoretical basis of the programming language Prolog and its various extensions. Logic programming is also fundamental to work in artificial intelligence, where it has been used for nonmonotonic (...) and commonsense reasoning, expert systems implementation, deductive databases, and applications such as computer-aided manufacturing. Krzysztof R. Apt is project leader at the Centre for Mathematics and Computer Science in Amsterdam and part-time Professor in Computer Science at the University of Amsterdam. Topics covered: Theory Foundations. Programming Languages. Implementation. Programming Methodologies and Tools. Applications. Deductive Databases. Artificial Intelligence. Parallelism. (shrink)

Doctoral programs at U.S. universities play a critical role in the development of human resources both in the United States and abroad. This volume reports the results of an extensive study of U.S. research-doctorate programs in five broad fields: physical sciences and mathematics, engineering, social and behavioral sciences, biological sciences, and the humanities. Research-Doctorate Programs in the United States documents changes that have taken place in the size, structure, and quality of doctoral education since the widely used 1982 editions. This (...) update provides selected information on nearly 4,000 doctoral programs in 41 subdisciplines at 274 doctorate-granting institutions. This volume also reports the results of the National Survey of Graduate Faculty, which polled a sample of faculty for their views on the scholarly quality of program faculty and the effectiveness of doctoral programs in preparing research scholars/scientists. This much-anticipated update of such an essential reference will be useful to education administrators, university faculty, and students seeking authoritative information on doctoral programs. (shrink)

The First International Workshop brings together researchers from the theoretical ends of the logic programming and artificial intelligence communities to discuss their mutual interests. Logic programming deals with the use of models of mathematical logic as a way of programming computers, where theoretical AI deals with abstract issues in modeling and representing human knowledge and beliefs. One common ground is nonmonotonic reasoning, a family of logics that includes room for the kinds of variations that can be found (...) in human reasoning. Topics covered: Stable Semantics. Default Logic. AutoEpistemic Logic. Truth Maintenance Systems. Implementation Issues. Diagnosis. Applications. Inheritance Reasoning. Logics of Belief. Inconsistency and Non-Monotonicity. (shrink)

"An important contribution to contemporary jurisprudential debate and to legal thought more generally, Just Interpretations is far ahead of currently available work."--Peter Goodrich, author of Oedipus Lex "I was struck repeatedly by the clarity of expression throughout the book. Rosenfeld's description and criticism of the recent work of leading thinkers distinguishes his work within the legal theory genre. Furthermore, his own theory is quite original and provocative."--Aviam Soifer, author of Law and the Company We Keep.

This volume presents a collection of refereed papers reflecting the state of the art in the area of over-constrained systems. Besides 11 revised full papers, selected from the 24 submissions to the OCS workshop held in conjunction with the First International Conference on Principles and Practice of Constraint Programming, CP '95, held in Marseilles in September 1995, the book includes three comprehensive background papers of central importance for the workshop papers and the whole field. Also included is an introduction (...) by one of the volume editors together with a bibliography listing 243 entries. All in all this is a very useful reference book relevant for all researchers and practitioners interested in hierarchical, partial, and over-constrained systems. (shrink)

The purpose of this paper is to set forth a sense in which programs can and do explain behavior, and to distinguish from this a number of senses in which they do not. Once we are tolerably clear concerning the sort of explanatory strategy being employed, two rather interesting facts emerge; (1) though it is true that programs are "internally represented," this fact has no explanatory interest beyond the mere fact that the program is executed; (2) programs which are couched (...) in information processing terms may have an explanatory interest for a given range of behavior which is independent of physiological explanations of the same range of behavior. (shrink)

The conditions animals experience during the early developmental stages of their lives can have critical ongoing effects on their future health, welfare, and proper development. In this paper we draw on evolutionary theory to improve our understanding of the processes of developmental programming, particularly Predictive Adaptive Responses (PAR) that serve to match offspring phenotype with predicted future environmental conditions. When these predictions fail, a mismatch occurs between offspring phenotype and the environment, which can have long-lasting health and welfare effects. (...) Examples include metabolic diseases resulting from maternal nutrition and behavioral changes from maternal stress. An understanding of these processes and their evolutionary origins will help in identifying and providing appropriate developmental conditions to optimize offspring welfare. This serves as an example of the benefits of using evolutionary thinking within veterinary science and we suggest that in the same way that evolutionary medicine has helped our understanding of human health, the implementation of evolutionary veterinary science (EvoVetSci) could be a useful way forward for research in animal health and welfare. (shrink)

The difficulties of the biological taxonomy development are argued to have been historically associated with two main problems: 1) the problem of searching for essential features which was unachievable within the framework of empiric taxonomy andcould be solved as a part of the mature theory; 2) the problem of developing of a model of the biological object the remedies of which were developed only in the XX century. The author argues that both problems are associated with the development of classificatory (...) and system ontology and the relevant methodologies. The classificatory methodology from its inception is argued to have developed as a means of classification of biological diversity; furthermore it is claimed to have been assumed that the features representing classes possessed ontological nature that is they actually represent individual objects. The author concludes that taking into account the empiric nature of taxonomy that assumption turned to be false. In the modern taxonomy along with the classical approach a classificatory-system approach was developed. Fundamentally, it is a transition from the classical approach to the modern one which is held to imply the development of a system model of the study subject. (shrink)

Hilbert’s program was an ambitious and wide-ranging project in the philosophy and foundations of mathematics. In order to “dispose of the foundational questions in mathematics once and for all,” Hilbert proposed a two-pronged approach in 1921: first, classical mathematics should be formalized in axiomatic systems; second, using only restricted, “finitary” means, one should give proofs of the consistency of these axiomatic systems. Although Gödel’s incompleteness theorems show that the program as originally conceived cannot be carried out, it had many partial (...) successes, and generated important advances in logical theory and metatheory, both at the time and since. The article discusses the historical background and development of Hilbert’s program, its philosophical underpinnings and consequences, and its subsequent development and influences since the 1930s. (shrink)

One of the main objectives of an ethics program is to improve the ethical culture of an organization. To date, empirical research treats at least one of these concepts as a one-dimensional construct. This paper demonstrates that by conceptualizing both constructs as multi-dimensional, a more in-depth understanding of the relationship between the two concepts can be achieved. Through the employment of the Corporate Ethical Virtues Model, eight dimensions of ethical culture are distinguished. Nine components of an ethics program are identified. (...) To assess the relationship between ethics programs and ethical culture, a survey was conducted of 4,056 members of the U. S. working population. The results show that the relationships between the components of an ethics program and the dimensions of ethical culture differ in strength, nature, and significance. Implications for research and practice are discussed. (shrink)

All organizations have ethics programs which consist of both explicit and implicit parts. This paper defines corporate ethics programs and identifies a number of their components. Corporate ethics programs'' structural and behavioral dimensions are proposed which may allow further examination of such program components and their impacts. Finally, fifteen propositions are suggested which describe the influence of founder values, competitive pressures, leadership, and organizational problems on corporate ethics programs and the manageability of such programs.

Meta-programs, which treat other computer programs as data, include compilers, editors, simulators, debuggers, and program transformers. Because of the wide ranging applications, meta-programming has become a subject of considerable practical and theoretical interest. This book provides the first comprehensive view of topics in the theory and application of meta-programming, covering problems of representation and of soundness and correctness of interpreters, analysis and evaluation of meta-logic programs, and applications to sophisticated knowledge-based systems.Harvey Abramson is Reader in Computer Science at (...) the University of Bristol, England; M. H. Rogers is Professor of Computer Science, also at the University of Bristol. Meta-Programming in Logic Programming is in the series Logic Programming Research Reports and Notes, edited by Ehud Shapiro. (shrink)

Some properties are causally relevant for a certain effect, others are not. In this paper we describe a problem for our understanding of this notion and then offer a solution in terms of the notion of a program explanation.

Source: "This book addresses the fundamentals of machine ethics. It discusses abilities required for ethical machine reasoning and the programming features that enable them. It connects ethics, psychological ethical processes, and machine implemented procedures. From a technical point of view, the book uses logic programming and evolutionary game theory to model and link the individual and collective moral realms. It also reports on the results of experiments performed using several model implementations. Opening specific and promising inroads into the (...) terra incognita of machine ethics, the authors define here new tools and describe a variety of program-tested moral applications and implemented systems. In addition, they provide alternative readings paths, allowing readers to best focus on their specific interests and to explore the concepts at different levels of detail. Mainly written for researchers in cognitive science, artificial intelligence, robotics, philosophy of technology and engineering of ethics, the book will also be of general interest to other academics, undergraduates in search of research topics, science journalists as well as science and society forums, legislators and military organizations concerned with machine ethics.". (shrink)

This collection of current research on logic programming languages presents results from a three-year, ESPRIT-funded effort to explore the integration of the foundational issues of functional, logic, and object-oriented programming. It offers valuable insights into the fast-developing extensions of logic programming with functions, constraints, concurrency, and objects. Chapters are grouped according to the unifying themes of functional programming, constraint, logic programming, and object-oriented programming.

What psychological and philosophical significance should we attach to recent efforts at computer simulations of human cognitive capacities? In answering this question, I find it useful to distinguish what I will call "strong" AI from "weak" or "cautious" AI. According to weak AI, the principal value of the computer in the study of the mind is that it gives us a very powerful tool. For example, it enables us to formulate and test hypotheses in a more rigorous and precise fashion. (...) But according to strong AI, the computer is not merely a tool in the study of the mind; rather, the appropriately programmed computer really is a mind, in the sense that computers given the right programs can be literally said to. (shrink)

In this article, I argue that genomic programs are not substitutes for multi-causal molecular mechanistic explanations of inheritance, but abstract representations of the same sort as mechanism schemas already described in the philosophical literature. On this account, the program analogy is not reductionistic and does not ignore or underestimate the active contribution of epigenetic elements to phenotypes and development. Rather, genomic program representations specifically highlight the genomic determinants of inheritance and their organizational features at work in the wider context of (...) the mechanisms of genome expression. (shrink)

Taken at face value, a programming language is defined by a formal grammar. But, clearly, there is more to it. By themselves, the naked strings of the language do not determine when a program is correct relative to some specification. For this, the constructs of the language must be given some semantic content. Moreover, to be employed to generate physical computations, a programming language must have a physical implementation. How are we to conceptualize this complex package? Ontologically, what (...) kind of thing is it? In this paper, we shall argue that an appropriate conceptualization is furnished by the notion of a technical artifact. (shrink)

The article presents the reasons for which the issue of providing housing to low-income citizens has been a real challenge in Addis Ababa during the recent years and will continue to be, given that its population is growing extremely fast. It examines the tensions between the universal aspirations and the local realities in the case of some of Ethiopia’s most ambitious mass pro-poor housing schemes, such as the “Addis Ababa Grand Housing Program” (AAGHP), which was launched in 2004 and was (...) integrated in the “Integrated Housing Development Program” (IHDP) in 2006. The article argues that the quotidian practices of communities and their socio-economic and cultural characteristics are related to the spatial attributes of co-housing practices. Drawing upon the idea that there is a mutual correspondence between social and spatial structures, it places particular emphasis on the analysis of the IHDP and aims to show that to shape strategies that take into account the social and cultural aspects of daily life of the poor citizens of Addis Ababa, it is pivotal to invite them to take part in the decision-making processes regarding their resettlement. Departing from the fact that a large percentage of the housing supply in Addis Ababa consists of informal unplanned housing, the article also compares the commoning practices in kebele houses and condominium units. The former refers to the legal informal housing units owned by the government and rented to their dwellers, whereas the latter concerns the housing blocks built in the framework of the IHDP for the resettlement of the kebele dwellers. The article analyzes these processes of resettlement, shedding light of the fact that kebele houses were located at the inner city, whereas the condominiums are located in the suburbs. Despite the fact that the living conditions in the condominium units are of a much higher quality than those in the kebele houses, their design underestimated or even neglected the role of the commoning practices. The article highlights the advantages of commoning practices in architecture and urban planning, and how the implementation of participation-oriented solutions can respond to the difficulties of providing housing. It argues that understanding the significance of the endeavors that take into account the opinions of dwellers during the phase of decision-making goes hand in hand with considering commoning practices as a source of architecture and urban planning frameworks for low-cost housing in this specific context. The key argument of the article is that urban planning and architecture solutions in Addis Ababa should be based on the principles of the so-called “negotiated planning” approach, which implies a close analysis of the interconnections between planning, infrastructure, and land. (shrink)

Companies offer ethics codes and training to increase employees’ ethical conduct. These programs can also enhance individual work attitudes because ethical organizations are typically valued. Socially responsible companies are likely viewed as ethical organizations and should therefore prompt similar employee job responses. Using survey information collected from 313 business professionals, this exploratory study proposed that perceived corporate social responsibility would mediate the positive relationships between ethics codes/training and job satisfaction. Results indicated that corporate social responsibility fully or partially mediated the (...) positive associations between four ethics program variables and individual job satisfaction, suggesting that companies might better manage employees’ ethical perceptions and work attitudes with multiple policies, an approach endorsed in the ethics literature. (shrink)

Companies offer ethics codes and training to increase employees' ethical conduct. These programs can also enhance individual work attitudes because ethical organizations are typically valued. Socially responsible companies are likely viewed as ethical organizations and should therefore prompt similar employee job responses. Using survey information collected from 313 business professionals, this exploratory study proposed that perceived corporate social responsibility would mediate the positive relationships between ethics codes/training and job satisfaction. Results indicated that corporate social responsibility fully or partially mediated the (...) positive associations between four ethics program variables and individual job satisfaction, suggesting that companies might better manage employees' ethical perceptions and work attitudes with multiple policies, an approach endorsed in the ethics literature. (shrink)

ABSTRACT:We analyze corporate ethics programs as control systems, arguing that how control is exercised may have pernicious consequences and be morally problematic. In particular, the control cultivated by ethics programs may weaken employees’ ability and motivation to exercise their own moral judgment, especially in novel situations. We develop this argument first by examining how organization theorists analyze control as an instrument of management coordination, and by addressing the political implications of control. We discuss coercive and enabling control as variations that (...) help account for the distinction between compliance-based ethics programs and values-based ethics programs. We then explore three potential drawbacks of ethics programs: the specter of indoctrination, a politicization of ethics, and an atrophy of competence. Ethics programs that rely on coercive control may undermine their own effectiveness at stemming misbehavior. (shrink)

Programmed cell death (PCD) in unicellular organisms is in some instances an altruistic trait. When the beneficiaries are clones or close kin, kin selection theory may be used to explain the evolution of the trait, and when the trait evolves in groups of distantly related individuals, group or multilevel selection theory is invoked. In mixed microbial communities, the benefits are also available to unrelated taxa. But the evolutionary ecology of PCD in communities is poorly understood. Few hypotheses have been offered (...) concerning the community role of PCD despite its far-reaching effects. The hypothesis we consider here is that PCD is a black queen. The Black Queen Hypothesis (BQH) outlines how public goods arising from a leaky function are exploited by other taxa in the community. Black Queen (BQ) traits are essential for community survival, but only some members bear the cost of possessing them, while others lose the trait In addition, BQ traits have been defined in terms of adaptive gene loss, and it is unknown whether this has occurred for PCD. Our conclusion is that PCD fulfils the two most important criteria of a BQ (leakiness and costliness), but that more empirical data are needed for assessing the remaining two criteria. In addition, we hold that for viewing PCD as a BQ, the original BQH needs to include social traits. Thus, despite some empirical and conceptual shortcomings, the BQH provides a helpful avenue for investigating PCD in microbial communities. (shrink)

Board composition, insider participation on compensation committees, and director compensation practices can potentially cause conflicts of interest between directors and shareholders. If these corporate governance structures result in situations where actions beneficial to directors do not also benefit shareholders, then shareholders may suffer.Corporate ethics programs usually address conflicts of interest that may arise in the firm''s activities. Some boards of directors take active roles in their firms'' ethics programs by actively overseeing the programs. This paper empirically examines the relationship between (...) ethics programs and potential conflicts of interest and the relationship between board involvement in a firm''s ethics program and potential conflicts of interest. (shrink)

The paper presents a refined method of extracting reasonable and sometimes unexpected programs from classical proofs of formulas of the form ∀x∃yB . We also generalize previously known results, since B no longer needs to be quantifier-free, but only has to belong to a strictly larger class of so-called “goal formulas”. Furthermore we allow unproven lemmas D in the proof of ∀x∃yB , where D is a so-called “definite” formula.

The notion of program verification appears to trade upon an equivocation. Algorithms, as logical structures, are appropriate subjects for deductive verification. Programs, as causal models of those structures, are not. The success of program verification as a generally applicable and completely reliable method for guaranteeing program performance is not even a theoretical possibility.

The author narrates briefly the friendship that developed from his instruction of James Dean in the art of photography and documents the Dean personality with exclusive portraits.

University program dropout is a problem that has important consequences not only for the student that leaves but also for the institution in which the withdrawal occurs. Therefore, higher education institutions must study the problem in greater depth to establish appropriate prevention measures in the future. However, most research papers currently focus primarily on the characteristics of students who leave university, rather than on those who choose to pursue alternative courses of study and therefore fail to take into account the (...) different kinds of abandonment. The aim of this paper is to identify the different types of dropout to define their characteristics and propose some recommendations. Thus, an ex post facto study was carried out on a sample of 1311 freshmen from a university in the north of Spain using data gathered using an ad-hoc designed questionnaire, applied by telephone or an online survey, and completed with data available in the university data warehouse. A descriptive analysis was performed to characterize the sample and identify five different groups, including 1. Students persisting in their initiated degree 2. Students who change of program (within the same university) 3. Students transferring to a different university 4. Students enrolling in non-higher-education studies 5. Students that quit studying. Also, data mining techniques (decision trees) were applied to classify the cases and generate predictive models to aid in the design of differentiated intervention strategies for each of the corresponding groups. (shrink)

In recent years, several formalisms for program construction have appeared. One such formalism is the type theory developed by Per Martin-L f. Well suited as a theory for program construction, it makes possible the expression of both specifications and programs within the same formalism. Furthermore, the proof rules can be used to derive a correct program from a specification as well as to verify that a given program has a certain property. This book contains a thorough introduction to type theory, (...) with information on polymorphic sets, subsets, monomorphic sets, and a full set of helpful examples. (shrink)

We document the influence on programming language semantics of the Platonism/formalism divide in the philosophy of mathematics.

We define a program size complexity function $H^\infty$ as a variant of the prefix-free Kolmogorov complexity, based on Turing monotone machines performing possibly unending computations. We consider definitions of randomness and triviality for sequences in ${\{0,1\}}^\omega$ relative to the $H^\infty$ complexity. We prove that the classes of Martin-Löf random sequences and $H^\infty$-random sequences coincide and that the $H^\infty$-trivial sequences are exactly the recursive ones. We also study some properties of $H^\infty$ and compare it with other complexity functions. In particular, $H^\infty$ (...) is different from $H^A$, the prefix-free complexity of monotone machines with oracle A. (shrink)

We construct logical languages which allow one to represent a variety of possible types of changes affecting the information states of agents in a multi-agent setting. We formalize these changes by defining a notion of epistemic program. The languages are two-sorted sets that contain not only sentences but also actions or programs. This is as in dynamic logic, and indeed our languages are not significantly more complicated than dynamic logics. But the semantics is more complicated. In general, the semantics of (...) an epistemic program is what we call aprogram model. This is a Kripke model of ‘actions’,representing the agents' uncertainty about the current action in a similar way that Kripke models of ‘states’ are commonly used in epistemic logic to represent the agents' uncertainty about the current state of the system. Program models induce changes affecting agents' information, which we represent as changes of the state model, called epistemic updates. Formally, an update consists of two operations: the first is called the update map, and it takes every state model to another state model, called the updated model; the second gives, for each input state model, a transition relation between the states of that model and the states of the updated model. Each variety of epistemic actions, such as public announcements or completely private announcements to groups, gives what we call an action signature, and then each family of action signatures gives a logical language. The construction of these languages is the main topic of this paper. We also mention the systems that capture the valid sentences of our logics. But we defer to a separate paper the completeness proof. (shrink)

In this paper I attempt to cast the current program verification debate within a more general perspective on the methodologies and goals of computer science. I show, first, how any method involved in demonstrating the correctness of a physically executing computer program, whether by testing or formal verification, involves reasoning that is defeasible in nature. Then, through a delineation of the senses in which programs can be run as tests, I show that the activities of testing and formal verification do (...) not necessarily share the same goals and thus do not always constitute alternatives. The testing of a program is not always intended to demonstrate a program's correctness. Testing may seek to accept or reject nonprograms including algorithms, specifications, and hypotheses regarding phenomena. The relationship between these kinds of testing and formal verification is couched in a more fundamental relationship between two views of computer science, one properly containing the other. (shrink)

This note presents a point of view upon the notions of programsubstitution which are the tools for proving properties of programs of algorithmic logics [5], [3] being sufficiently strong and universal to comprise almost all previously introduced theories of programming, and the so-called extended algorithmic logic [1], [2] and algorithmic logic with nondeterministic programs [4]. It appears that the mentioned substitution rule allows us to examine more deeply algorithmic properties of terms, formulas and programs. Besides the problem of Post-completeness (...) and structural completeness of algorithmic logics strengthened additionally by the rule of substitution is raised. (shrink)

In these essays the minimalist approach to linguistic theory is formulated and progressively developed.

A proof of ‘correctness’ for a mathematical algorithm cannot be relevant to executions of a program based on that algorithm because both the algorithm and the proof are based on assumptions that do not hold for computations carried out by real-world computers. Thus, proving the ‘correctness’ of an algorithm cannot establish the trustworthiness of programs based on that algorithm. Despite the (deceptive) sameness of the notations used to represent them, the transformation of an algorithm into an executable program is a (...) wrenching metamorphosis that changes a mathematical abstraction into a prescription for concrete actions to be taken by real computers. Therefore, it is verification of program executions (processes) that is needed, not of program texts that are merely the scripts for those processes. In this view, verification is the empirical investigation of: (a) the behavior that programs invoke in a computer system and (b) the larger context in which that behavior occurs. Here, deduction can play no more, and no less, a role than it does in the empirical sciences. (shrink)

This paper describes formalizations of Tait's normalization proof for the simply typed λ-calculus in the proof assistants Minlog, Coq and Isabelle/HOL. From the formal proofs programs are machine-extracted that implement variants of the well-known normalization-by-evaluation algorithm. The case study is used to test and compare the program extraction machineries of the three proof assistants in a non-trivial setting.

How are the properties of computer programs proved? We discuss three approaches in this article: inductive invariants, functional semantics, and explicit semantics. Because the first approach has received by far the most attention, it has produced the most impressive results to date. However, the field is now moving away from the inductive invariant approach.

Our aim in this paper is to evaluate Frank Jackson and Philip Pettit’s ‘program explanation’ framework as an account of the autonomy of the special sciences. We argue that this framework can only explain the autonomy of a limited range of special science explanations. The reason for this limitation is that the framework overlooks a distinction between two kinds of properties, which we refer to as ‘higher-level’ and ‘higher-order’ properties. The program explanation framework can account for the autonomy of special (...) science explanations that appeal to higher-level properties but it does not account for the autonomy of most of those explanations that appeal to higher-order properties. (shrink)