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)

One of the distinguishing features of mathematics is the exceptional level of consensus among mathematicians. However, an analysis of what mathematicians agree on, how they achieve this agreement, and the relevant historical conditions is lacking. This paper is a programmatic intervention providing a preliminary analysis and outlining a research program in this direction.First, I review the process of ‘negotiation’ that yields agreement about the validity of proofs. This process most often does generate consensus, however, it may give rise to (...) another kind of disagreement: whether the original and new proof are effectively the same, leading to potential disagreement about the validity of the original proof.Second, I historicize the phenomenon of consensus. I show that in earlier European mathematics and other mathematical cultures, consensus about the validity of arguments was substantially weaker or conceived differently than it is today. This means that contemporary consensus about the validity of mathematical proofs should be explained by historical changes in mathematical practice.Finally, I conjecture what brought about the contemporary form of mathematical consensus. Since a sharp rise in consensus occurs around the turn of the 20th century, it makes sense to explain this consensus by the concurrent formalization of mathematics. However, this explanation has a major flaw: it explains a really existing phenomenon (consensus) by something that hardly ever happens (writing proofs in formal languages). I will therefore explain the ways in which formalization does enter mathematical practice so as to account for contemporary forms of mathematical consensus. (shrink)

In the article, philosophical and methodological analysis of the program of Hilbert’s formalism as a really working direction for consideration of the bases of modern mathematics is presented. For the professional mathematicians methodological advantages of the program of formalism advanced by David Hilbert, consist primarily in the fact that the highest possible level of theoretical rigor of modern mathematical theories was practically represented there. To resolve the fundamental difficulties of the problem of bases of mathematics, according to Hilbert, (...) the theory of mathematical proof is needed, but contrary to popular belief rigorous formalization of the proof is not a synonym of reliability and rigor of mathematical reasoning from the point of view of the philosophy of the foundations of mathematics. In fact, the consistency of the theories is "more important" than their logical consistency because not every statement, which does not contradict to the reasonable ones, can be attributed to a true statement. However, for working mathematicians, Hilbert is logical and consistent and the axiomatic method and formalism are an essential part of their rules of thinking. (shrink)

Aidan Lyon has recently argued that some mathematical explanations of empirical facts can be understood as program explanations. I present three objections to his argument.

The first part of the paper introduces the varieties of modern constructive mathematics, concentrating on Bishop's constructive mathematics (BISH). it gives a sketch of both Myhill's axiomatic system for BISH and a constructive axiomatic development of the real line R. The second part of the paper focusses on the relation between constructive mathematics and programming, with emphasis on Martin-L6f 's theory of types as a formal system for BISH.

The first part of the paper introduces the varieties of modern constructive mathematics, concentrating on Bishop's constructive mathematics. it gives a sketch of both Myhill's axiomatic system for BISH and a constructive axiomatic development of the real line R. The second part of the paper focusses on the relation between constructive mathematics and programming, with emphasis on Martin-L6f 's theory of types as a formal system for BISH.

Most scholars think of David Hilbert's program as the most demanding and ideologically motivated attempt to provide a foundation for mathematics, and because they see technical obstacles in the way of realizing the program's goals, they regard it as a failure. Against this view, Curtis Franks argues that Hilbert's deepest and most central insight was that mathematical techniques and practices do not need grounding in any philosophical principles. He weaves together an original historical account, philosophical analysis, and his own (...) development of the meta-mathematics of weak systems of arithmetic to show that the true philosophical significance of Hilbert's program is that it makes the autonomy of mathematics evident. The result is a vision of the early history of modern logic that highlights the rich interaction between its conceptual problems and technical development. (shrink)

An Essay on Mathematical Instrumentalism M. Detlefsen. THE PHILOSOPHICAL FUNDAMENTALS OF HILBERT'S PROGRAM 1. INTRODUCTION In this chapter I shall attempt to set out Hilbert's Program in a way that is more revealing than ...

applied, for instance, to developing a decision support system for the Space Shuttle INogueira et al., 2001] and to graph-theoretic problems arising in..

The issue of proper functioning of operative computing and the utility of program verification, both in general and of specific methods, has been discussed a lot. In many of those discussions, attempts have been made to take mathematics as a model of knowledge and certitude achieving, and accordingly infer about the suitable ways to handle computing. I shortly review three approaches to the subject, and then take a stance by considering social factors which affect the epistemic status of both (...) mathematics and computing. I use the analogy between mathematics and computing in reverse—that is to say, I consider operative computing as a form of making mathematics, and so attempt to learn from computing to mathematics in general. I conclude that mathematics engineering is a field to be both developed for practical improvement of doing mathematics and taken into consideration while philosophizing about mathematics as well. (shrink)

Teaching mathematics and improving mathematics competence are pending subjects within our educational system. The PEIM (Programa Evolutivo Instruccional para Matemáticas), a constructivist intervention program for the improvement of mathematical performance, affects the different agents involved in math learning, guaranteeing a significant improvement in students’ performance. The program is based on the following pillars: (a) students become the main agents of their learning by constructing their own knowledge; (b) the teacher must be the guide to facilitate and guarantee such (...) a construction by being a great connoisseur of the fundamental aspects of the development of the child’s mathematical thinking; (c) the mathematical contents must be sequenced in terms of the complexity and significance for the student as well as contextualized at all times; and (d) the classroom must have a constructivist climate highlighting cooperative work among students. The implementation of PEIM along with the empirical evaluation conducted in several centers in Madrid and Zaragoza (Spain) confirm how students improve their mathematical competence. Both first- and second-grade students in elementary education were far more effective in solving problems, highlighting the use of more advanced strategies in their resolution and a lower incidence of conceptual errors. Moreover, it was possible to verify how the students proving greater difficulty, experienced an evolution in learning similarly to those who did not present it. The program provides customized education to allow the teacher to know at all times how he should be more influential on the students’ learning through mathematical profiles. Both teaching practice and teachers were observed, being that of the experimental group more prone to analyzing processes and allowing the construction of knowledge by students, due to their psycho-developmental training. As a result, we found several improvements through the implementation of the program that may serve, for upcoming years, as a basis for the necessary changes in the teaching of mathematics. (shrink)

In the debate over whether mathematical facts, properties, or entities explain physical events (in what philosophers call “extra-mathematical” explanations), Aidan Lyon’s (2012) affirmative answer stands out for its employment of the program explanation (PE) methodology of Frank Jackson and Philip Pettit (1990). Juha Saatsi (2012; 2016) objects, however, that Lyon’s examples from the indispensabilist literature are (i) unsuitable for PE, (ii) nominalizable into non-mathematical terms, and (iii) mysterious about the explanatory relation alleged to obtain between the PE’s mathematical explanantia and (...) physical explananda. In this paper, I propose a counterexample to Saatsi’s objections. My counterexample is Frank Jackson’s (1998a) program explanation for color experience, which I argue needs recasting as an extra-mathematical PE due to its implicit reliance on reflectance, a property that suffers conceptual regress unless redefined with Fourier harmonics. Pace Saatsi, I argue that this recast example is an authoritative PE, non-nominalizable, and minimally esoteric. Important for the indispensability debate at large, moreover, is that my counterexample reifies Fourier harmonics without the Enhanced Indispensability Argument (an argument to which Lyon applies PE as a premise). Indispensabilists have long overlooked the conditionalization of a limited mathematical realism on property realism, and my counterexample to Saatsi exploits this conditionalization. (shrink)

The most prominent “schools” or programs for the foundations of mathematics that took shape in the first third of the 20th century emerged directly from, or in response to, developments in mathematics and logic in the latter part of the 19th century. The first of these programs, so-called logicism, had as its aim the reduction of mathematics to purely logical principles. In order to understand properly its achievements and resulting problems, it is necessary to review the background (...) from that previous period. (shrink)

We investigate the strength of the existence of a non-principal ultrafilter over fragments of higher-order arithmetic. Let [Formula: see text] be the statement that a non-principal ultrafilter on ℕ exists and let [Formula: see text] be the higher-order extension of ACA0. We show that [Formula: see text] is [Formula: see text]-conservative over [Formula: see text] and thus that [Formula: see text] is conservative over PA. Moreover, we provide a program extraction method and show that from a proof of a strictly (...) [Formula: see text] statement ∀ f ∃ g A qf in [Formula: see text] a realizing term in Gödel's system T can be extracted. This means that one can extract a term t ∈ T, such that ∀ f A qf). (shrink)

The design of the following paper is to establish an interpretative link between Kant’s transcendental philosophy and Hilbert’s foundational program. Through a regressive reading of Kant’s Critique of Pure Reason (1781), we can see the motivation of his philosophical project as bound with the task to expose the a priori presuppositions which are the grounds for the possibility of actual knowledge claims. Moreover, according to him the sole justification for such procedure is the (informal) proof of consistency and (architectonical) completeness. (...) Hilbert tried to strip Kant’s philosophy of its last anthropomorphic vestiges which led to the formulation of his “finite standpoint” and the prooftheoretical methods for axiomatic reconstruction of classical mathematics. Therefore, contrary to the received view, the proofs of consistency and completeness which were envisaged as part of his metamathematical program were not conceived as a means to secure to epistemic basis of mathematical knowledge. Accordingly, the program itself was not confuted by Gödel’s theorems and remains as viable as ever. (shrink)

Mathematical logic is a branch of mathematics that takes axiom systems and mathematical proofs as its objects of study. This book shows how it can also provide a foundation for the development of information science and technology. The first five chapters systematically present the core topics of classical mathematical logic, including the syntax and models of first-order languages, formal inference systems, computability and representability, and Gödel’s theorems. The last five chapters present extensions and developments of classical mathematical logic, particularly (...) the concepts of version sequences of formal theories and their limits, the system of revision calculus, proschemes (formal descriptions of proof methods and strategies) and their properties, and the theory of inductive inference. All of these themes contribute to a formal theory of axiomatization and its application to the process of developing information technology and scientific theories. The book also describes the paradigm of three kinds of language environments for theories and it presents the basic properties required of a meta-language environment. Finally, the book brings these themes together by describing a workflow for scientific research in the information era in which formal methods, interactive software and human invention are all used to their advantage. The second edition of the book includes major revisions on the proof of the completeness theorem of the Gentzen system and new contents on the logic of scientific discovery, R-calculus without cut, and the operational semantics of program debugging. This book represents a valuable reference for graduate and undergraduate students and researchers in mathematics, information science and technology, and other relevant areas of natural sciences. Its first five chapters serve as an undergraduate text in mathematical logic and the last five chapters are addressed to graduate students in relevant disciplines. (shrink)

Reverse mathematics is a program in mathematical logic that seeks to give precise answers to the question of which axioms are necessary in order to prove theorems of "ordinary mathematics": roughly speaking, those concerning structures that are either themselves countable, or which can be represented by countable "codes". This includes many fundamental theorems of real, complex, and functional analysis, countable algebra, countable infinitary combinatorics, descriptive set theory, and mathematical logic. This entry aims to give the reader a broad (...) introduction to the history, methodology, and results of the reverse mathematics program, with a particular focus on its connections to foundational programs such as finitism, constructivism, and predicativism. (shrink)

Creativity is an essential factor in ensuring the sustainable development of a society. Improving students’ creativity has gained much attention in education, especially in Science, Technology, Engineering, Arts, and Mathematics education. In a quasi-experimental design, this study examines the effectiveness of a project-based STEAM program on the development of creativity in Chinese elementary school science education. We selected two fourth-graders classes. One received a project-based STEAM program, and the other received a conventional science teaching over 6 weeks. Students’ creativity (...) was assessed before and after the intervention using a multi-method approach, including a test of divergent thinking, a story completion through the Consensus Assessment Technique, a creative self-efficacy measure, and a group-based creative project. Moreover, all students received a test of their science knowledge after the intervention. The results showed that compared with the control group, the creativity of the experimental group students improved significantly for 6 weeks at both individual and group level, even though their knowledge in science were comparable. This result confirmed the effectiveness of a project-based STEAM educational program improving elementary school students’ creativity. Implications are discussed. (shrink)

Purpose: This study aimed to explore the relationship between mathematic achievement and programming self-efficacy, and adopt a mediation model to verify the mediating role of creativity on the relationship between mathematic achievement and programming self-efficacy.Methods: A total of 950 upper-secondary school students were surveyed using their math test scores, the Kirton Adaption-Innovation and the Programmed Self-Efficacy Scale. SPSS-26 was used for descriptive statistical analysis and correlation analysis of related variables. The PROCESS plugin was used to test the mediating (...) effect of creativity.Results: Mathematic achievement has a positive effect on programming self-efficacy, mathematic achievement is positively related to creativity, and creativity also has a positive influence on programming self-efficacy. Creativity has a mediating effect on the relationship between mathematic achievement and programming self-efficacy.Conclusion: The results revealed that mathematic achievement affected programming self-efficacy directly and also indirectly through creativity. This provided certain ideas for the development of programming education for teenagers. Since students’ mathematics learning and creativity are related to programming learning, it is necessary to pay attention to the integration of the disciplines of programming education and mathematics. Further, the cultivation of innovative thinking is also critical to facilitate programming learning. (shrink)

Logic has pride of place in mathematics and its 20th century offshoot, computer science. Modern symbolic logic was developed, in part, as a way to provide a formal framework for mathematics: Frege, Peano, Whitehead and Russell, as well as Hilbert developed systems of logic to formalize mathematics. These systems were meant to serve either as themselves foundational, or at least as formal analogs of mathematical reasoning amenable to mathematical study, e.g., in Hilbert’s consistency program. Similar efforts continue, (...) but have been expanded by the development of sophisticated methods to study the properties of such systems using proof and model theory. In parallel with this evolution of logical formalisms as tools for articulating mathematical theories (broadly speaking), much progress has been made in the quest for a mechanization of logical inference and the investigation of its theoretical limits, culminating recently in the development of new foundational frameworks for mathematics with sophisticated computer-assisted proof systems. In addition, logical formalisms developed by logicians in mathematical and philosophical contexts have proved immensely useful in describing theories and systems of interest to computer scientists, and to some degree, vice versa. Three examples of the influence of logic in computer science are automated reasoning, computer verification, and type systems for programming languages. (shrink)

The quality of doctoral-level chemistry (N=145), computer science (N=58), geoscience (N=91), mathematics (N=115), physics (N=123), and statistics/biostatistics (N=64) programs at United States universities was assessed, using 16 measures. These measures focused on variables related to: program size; characteristics of graduates; reputational factors (scholarly quality of faculty, effectiveness of programs in educating research scholars/scientists, improvement in program quality during the last 5 years); university library size; research support; and publication records. Chapter I discusses prior attempts to assess quality in graduate (...) education, development of the study plans, and the selection of disciplines and programs to be evaluated. Chapter II discusses the methodology used, focusing on each of the assessment measures. Chapters III to VIII present, respectively, findings from the analyses of the chemistry, computer science, geoscience, mathematics, physics, and statistics/biostatistics programs. Chapter IX includes a summary of results, correlations among measures, several additional analyses, and suggestions for future studies. Among the findings reported are those indicating that mathematics programs had, on the average, the largest number of faculty (N=33) in December 1980 followed closely by physics (N=28) and chemistry (N=23), and that 80 percent of computer science students had job commitments by graduation. (Survey instruments and supporting documentation are included in appendices.) (JN). (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)

Our program is ambitious, as is any attempt to match life (in our case real science) with virtue (e.g., exactness). We want our semantics to be not only simia mathematicae but also ancilla scientiae: built more geometrico and at the same time relevant, nay useful, to live science. The goal of exactness may sound arrogant but is actually modest, for the more we rigorize the more we are forced to leave out of consideration, at least for the time being. As (...) to the service intention: we should try to be of some help to science because the latter faces semantic problems but has no tools of its own for solving them. If it had such tools scientists would not engage in spirited polemics over matters of sense and reference, as they often do. Witness the debates on whether the relativistic and quantum theories are concerned with sentient observers, whether population genetics refers to populations taken as wholes, whether psychology is actually concerned with the brain, and whether the sense of a theory is excreted by its mathematical formalism or is determined by the way the theory is tested.A semantics of science should help settle these and similar issues. Moreover it should give sound advice as to how to formulate scientific theories so as to avoid such imprecisions and ambiguities as may give rise to debates of the kind. Constructing such a semantics, both exact and relevant to science, should be more rewarding than either manufacturing neat but irrelevant theories or pursuing erratic polemics on meaning and meaning changes. Research supported by a Killam grant awarded by the Canada Council. (shrink)