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.

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.

Let ${2-\textsf{RAN}}$ be the statement that for each real X a real 2-random relative to X exists. We apply program extraction techniques we developed in Kreuzer and Kohlenbach (J. Symb. Log. 77(3):853–895, 2012. doi:10.2178/jsl/1344862165), Kreuzer (Notre Dame J. Formal Log. 53(2):245–265, 2012. doi:10.1215/00294527-1715716) to this principle. Let ${{\textsf{WKL}_0^\omega}}$ be the finite type extension of ${\textsf{WKL}_0}$ . We obtain that one can extract primitive recursive realizers from proofs in ${{\textsf{WKL}_0^\omega} + \Pi^0_1-{\textsf{CP}} + 2-\textsf{RAN}}$ , i.e., if ${{\textsf{WKL}_0^\omega} + \Pi^0_1-{\textsf{CP}} (...) + 2-\textsf{RAN} \, {\vdash} \, \forall{f}\, {\exists}{x} A_{qf}(f,x)}$ then one can extract from the proof a primitive recursive term t(f) such that ${A_{qf}(f,t(f))}$ . As a consequence, we obtain that ${{\textsf{WKL}_0}+ \Pi^0_1 - {\textsf{CP}} + 2-\textsf{RAN}}$ is ${\Pi^0_3}$ -conservative over ${\textsf{RCA}_0}$. (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)

Volume 20, Issue 7, July 2020, Page 89-92.

We introduce a new type system called “System ST” , based on subtyping, and prove the basic property of the system. We show the extraordinary expressive power of the system which leads us to think that it could be a good candidate for doing both proof and extraction of programs.

In their open peer commentary: “Making It Count: Extracting Real World Data from Compassionate Use and Expanded Access Programs”, Rozenberg and Greenbaum discuss impo...

We prove constructively that for any propositional formula in Conjunctive Normal Form, we can either find a satisfying assignment of true and false to its variables, or a refutation of showing that it is unsatisfiable. This refutation is a resolution proof of ¬. From the formalization of our proof in Coq, we extract Robinson’s famous resolution algorithm as a Haskell program correct by construction. The account is an example of the genre of highly readable formalized mathematics.

This article generalises the refined A-translation method for extracting programs from classical proofs [U. Berger,W. Buchholz, H. Schwichtenberg, Refined program extraction from classical proofs, Annals of Pure and Applied Logic 114 3–25] to the scenario where additional assumptions such as choice principles are involved. In the case of choice principles, this is done by adding computational content to the ‘translated’ assumptions, an idea which goes back to [S. Berardi, M. Bezem, T. Coquand, On the computational content of the (...) axiom of choice, JSL 63 600–622] and has been further elaborated in [U. Berger, P. Oliva, Modified bar recursion and classical dependent choice, in: M. Baaz, S.D. Friedman, J. Kraijcek , Logic Colloquium ’01, in: Lecture Notes in Logic, vol. 20, Springer, Berlin, 2005, pp. 89–107]. We further investigate the applicability of this extension by means of a small but non-trivial example, and discuss the formalisation as well as some optimisations necessary in order to extract terminating programs. Both formalisation and term extraction have been implemented in the interactive proof assistant Minlog. (shrink)

Research regarding ethics programs represents an important segment of business ethics literature. In the last thirty years, scientific discourse on ethics programs has flourished. Numerous studies examined their functions, composition, application in organizational practice, and impact on employee ethical behavior and many other organizational variables. However, so far there has been no study that would comprehensively map this particular field. Given that, this paper aims to examine discourse on ethics programs in its complexity within business and management literature. Based on (...) a sophistically composed search protocol in the Scopus database, and after multiple rounds of checks, we extracted a final sample of 287 documents that matched the selection criteria. The sample was thoroughly analyzed by means of advanced bibliometric analytics tools. The results show the quantitative impact of ethics program literature via publication and citation metrics, a network of co-occurring themes and clusters of scientific inquiry, and the evolution of respective discourse over time. This detailed analysis results in a set of conclusions provided in the last part of the paper summarizing the quantitative performance and thematic scope of literature on ethics programs. (shrink)

forcement learning algorithms that generate only reactive policies and existing probabilistic planning algorithms that requires a substantial amount of a priori knowledge in order to plan we devise a two stage bottom up learning to plan process in which rst reinforcement learn ing dynamic programming is applied without the use of a priori domain speci c knowledge to acquire a reactive policy and then explicit plans are extracted from the learned reactive policy Plan extraction is based on a beam (...) search algorithm that performs temporal projection in a restricted fashion guided by the value functions resulting from reinforcement learn ing dynamic programming.. (shrink)

Conventional wisdom among comparative political economists maintains that the participation of employers in policymaking and policy implementation, fostered by corporatist arrangements, is crucial to the successful expansion of active labor market policy. This article introduces a transaction-oriented theory of corporatism, partisanship, and ALMP that challenges the dominant view. It argues that corporatist arrangements do not affect the overall scope of ALMP but facilitate particular types of ALMP programs, ones that require the joint participation of employers and the state and involve (...) a transfer of public resources to employers. Corporatist arrangements facilitating such programs—which center-right parties tend to prefer over those produced unilaterally by the state—also shift the focus of partisan conflict over ALMP from the level of public expenditure to the structure. Evidence for these claims is provided by time-series cross-sectional analyses of twenty-one OECD countries since the mid-1980s. (shrink)

Big data has brought about opportunities for landscape architecture, changing the design thinking of layout optimization simulation, expanding the platform for public participation in layout optimization simulation design, reflecting social and humanistic care, and promoting the integration of discipline cooperation and data. At the same time, it also brings about challenges. The proposal of data theory, the acquisition and analysis of data, and the protection of privacy are all issues that we need to face and solve. First, build a layout (...) optimization simulation program under the background of big data. Follow the procedures of conventional layout optimization simulation, add big data analysis technology to the preliminary analysis, layout optimization simulation design, and later evaluation management, introduce new data processing methods, and build a theoretical framework of landscape optimization simulation methods that integrate new and traditional data. Second, studying the evolution of the landscape image layout of the three-dimensional pastoral complex is different: the overall landscape image layout of the three-dimensional pastoral complex shows a trend of fragmentation and heterogeneity. Among them, the arable land is gradually fragmented, the wetland and water area are simplified in form, the woodland and grassland patches are gradually distributed, the fragmentation is reduced by 76.19%, and the connectivity index is gradually increased. From a spatial perspective, the edge area outside the Fourth Ring Road becomes the most obvious area of fragmentation tendency. Finally, by introducing big data into the landscape layout optimization simulation, a layout optimization simulation method based on big data is constructed and used in the layout optimization simulation of the landscape image layout of the three-dimensional pastoral complex to guide the participatory layout optimization simulation. (shrink)

One of the least studied aspects of programs of reparation, both in theory and in practice, is financing. This is odd given the fact that mobilizing resources, both domestic and foreign, is politically one of the most difficult tasks any society can undertake. This paper centers on the subject of financing reparation programs and attempts to answer the following questions: Which factors play a role in the process of mobilizing domestic and foreign resources to finance reparations? Is financing solely a (...) technical-economic problem, or does it involve political, social, and cultural factors? Why do governments prefer financing social programs instead of programs of reparation? How do the proposals made by truth commissions regarding financing affect the viability of programs of reparation? Which factors explain the efficacy of financing models of reparation programs? In order to address these questions, the paper has been divided into three main sections. In the first, programs of reparation are analyzed from the perspective of political economy, which means that both economic and non-economic factors that influence the mobilization of domestic and foreign resources by a transitional society are taken into consideration. The second section focuses on international experiences in the area of financing programs of reparation, with the purpose of extracting some lessons. The third section presents the main conclusions of the study. (shrink)

One of the least studied aspects of programs of reparation, both in theory and in practice, is financing. This is odd given the fact that mobilizing resources, both domestic and foreign, is politically one of the most difficult tasks any society can undertake. This paper centers on the subject of financing reparation programs and attempts to answer the following questions: Which factors play a role in the process of mobilizing domestic and foreign resources to finance reparations? Is financing solely a (...) technical-economic problem, or does it involve political, social, and cultural factors? Why do governments prefer financing social programs instead of programs of reparation? How do the proposals made by truth commissions regarding financing affect the viability of programs of reparation? Which factors explain the efficacy of financing models of reparation programs? In order to address these questions, the paper has been divided into three main sections. In the first, programs of reparation are analyzed from the perspective of political economy, which means that both economic and non-economic factors that influence the mobilization of domestic and foreign resources by a transitional society are taken into consideration. The second section focuses on international experiences in the area of financing programs of reparation, with the purpose of extracting some lessons. The third section presents the main conclusions of the study. (shrink)

Most current statistical natural language processing models use only local features so as to permit dynamic programming in inference, but this makes them unable to fully account for the long distance structure that is prevalent in language use. We show how to solve this dilemma with Gibbs sam- pling, a simple Monte Carlo method used to perform approximate inference in factored probabilistic models. By using simulated annealing in place of Viterbi decoding in sequence models such as HMMs, CMMs, and CRFs, (...) it is possible to incorporate non-local structure while preserving tractable inference. We use this technique to augment an existing CRF-based information extraction system with long-distance dependency models, enforcing label consistency and extraction template consistency constraints. This technique results in an error reduction of up to 9% over state-of-the-art systems on two established information extraction tasks. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Reviewed by:Just Sustainability: Technology, Ecology, and Resource Extraction eds. by Christiana Z. Peppard and Andrea ViciniTallessyn Zawn Grenfell-LeeJust Sustainability: Technology, Ecology, and Resource Extraction Edited by Christiana Z. Peppard and Andrea Vicini maryknoll, ny: orbis, 2015. 304 pp. $42.00Just Sustainability offers a detailed journey through various Catholic contextual understandings of what ecological sustainability means today in light of the demands of justice. In the first section of (...) the book, called "Locations" (11–53), the contributors put concepts of sustainability into dialog with concerns of socioeconomic, gender, and racial justice from contexts as diverse as Europe, East Asia, India, Africa, and North America. The various locations share common themes, such as the importance of deep meanings of the term "sustainability," the priority of education and advocacy, the resource and energy challenges behind structures of injustice, and the primary role of economics. Yet distinctive emphases emerge from the diverse contexts as well. Examples include the [End Page 200] need for humility instead of the ironic arrogance of nuclear energy in Japan, the widespread challenges of corruption in Africa and Mexico, and the problem of the agriculture lobby in the United States.The second section, "Structures" (57–156), steps back from specific cultural contexts and explores various systemic approaches to the challenge of just sustainability. Using Catholic social teachings, the authors again often speak from diverse global contexts, but with reference specifically to economic and societal systems such as politics, measurements of well-being, urban planning, food and agriculture, and health care. In this section the authors speak of which structures have worked and which have failed to build just and sustainable societies. For example, in the Philippines, more accountability through transparency and regular reporting helped impact energy efficiency. In Kenya and Chad, the authors highlight the need for reliable social systems of access, communication, collaboration, and government in order to counter corruption and build sustainable programs to address HIV, hunger, employment, and food sovereignty. Several authors also describe the positive impact of more democratic and egalitarian participatory structures that involve the people most affected by ecological decisions and policies.The last section, "Theological Stances and Sustainable Relations" (159–268), delves more deeply into Catholic theological resources to provide both a foundation as well as specific practices of just sustainability. The authors wrestle with theocentric, biocentric, and anthropocentric concepts of humanity and the imago Dei, the Eucharist as a potentially powerful way to connect ideas of inequity, the promise of ecofeminist theologies in elevating the wisdom of local peoples to build just sustainability practices, and virtue ethics and Catholic social teachings to foster ecological conversion and build solidarity, hope, and efficacy.The book sets itself a challenging task, to provide a coherent picture of Catholic approaches to building just sustainability while presenting a spectrum of not only diverse cultural and geographical contexts but also diverse theologies. In the end, the book reveals the ways in which Catholic laity and leaders are creatively responding to the challenge of just sustainability across much of the globe by using a combination of ecclesial, theological, and social scientific resources. The book would have benefited from a concluding essay to tie together some of the salient themes from the numerous, somewhat disparate essays, and a chapter from South America would have strengthened the global orientation of the collection. Nonetheless, the reader is left with a more holistic understanding of the difficult task of just sustainability as well as the wealth of work toward this goal from many parts of the Earth. [End Page 201]Tallessyn Zawn Grenfell-LeeBoston University School of TheologyCopyright © 2018 Society of Christian Ethics... (shrink)

Since the late nineties there has been an increased interested in probabilistic logic learning, an area within AI that combines machine learning with logic-based knowledge representation and uncertainty reasoning. Several different formalisms for combining first-order logic with probability reasoning have been proposed, and it has been studied how models in these formalisms can be automatically learned from data. -/- This talk starts with a brief introduction to probabilistic logic learning, after which we will focus on a relatively new formalism known (...) as CP-logic. CP-logic stands for “causal probabilistic logic”. It is a knowledge representation formalism that allows us to write down rules that indicate that a certain combination of conditions may cause certain effects with a particular probability (e.g., tossing a coin may cause a result of heads or tails, each with 50% probability). Besides the fact that this formalism is interesting for knowledge representation in itself, it also offers interesting opportunities from the machine learning point of view. Indeed, given the semantics of these CP-logic programs, learning them from data amounts to extracting probabilistic causal influences from data. We will discuss recent research on learning CP-logic programs, including: algorithms for learning them; how they relate to graphical models; and applications of learning CP-logic programs. (shrink)

In coal mining technology systems, it is very important to acquire, store, and represent basic geological data comprehensively and accurately. Based on the current working mode and information level in mining geology at coal mines, this paper proposes a process of building basic geological database for modeling of coal mines by using existing results’ data of mining geology and develops the efficient program for getting the basic geological data from the important 2D plane drawings’ achievement at mines, such as (...) the contour maps of mine coal seam floors, geological cross-sections, underground drilling results, and geological survey results, based on AutoLISP, which is a programming language for the secondary development of AutoCAD. The obtained data in general text format is stored and managed by the MongoDB database, which realizes the storage, query, analysis, and correction of massive data of geological objects in the space of the underground coalmine. The application results show that compared with the previous data acquisition methods such as manual input and graphic transformation attribute, the extraction of spatial and attribute data from the existing mine 2D plane drawings by programming can effectively avoid the prominent problems such as artificial gross error, distortion of graph conversion, and different database structure, make the obtained spatial geological data more comprehensive, accurate, and effective, and, meanwhile, increase the rate by more than 60%, which plays an important role in data support for the construction of the geological modeling systems for transparent mines. (shrink)

When Ockham's logic arrives in Italy, some Dominican philosophers bring into question Ockham's ontological reductionist program. Among them, Franciscus de Prato and Stephanus de Reate pay a great attention to refute Ockham's claim that no universal exists in the extra-mental world. In order to reject Ockham's program, they start by reconsidering the notion of 'real', then the range of application of the rational and the real distinction. Generally, their strategy consists in re-addressing against Ockham some arguments extracted from (...) Hervaeus Natalis's works. Franciscus's and Stephanus's basic idea is that some universals are not acts of cognition, but extra-mental, predicable things. Such things are not separable from singulars, nonetheless they are not the same as those singulars. Consequently, it is not necessary to allow, as Ockham does, that if two things are not really identical, they are really different and hence really separable. According to them, it is possible to hold that two things are not really identical without holding that they are also really non-identical and hence really different. Basically, their reply relies on a different notion of the relation of identity. Identity is regarded as an intersection of classes of things, so that it is possible to say that two things are really identical without saying that they also are the same thing. Franciscus and Stephanus, however, do not seem to achieve completely their aim. (shrink)

Background Advance care planning (ACP) is a process in which adults engage in an ongoing dialogue about future medical treatment and care. Though ACP is recommended to improve the quality of end-of-life care, the details of the dialogue experience in ACP are unknown. Objective To explore participants’ experiences of dialogue in an ACP educational program that encouraged them to discuss the value of a way of life. Research design This qualitative descriptive study used the focus group interview method. Data (...) were analyzed using qualitative content analysis. Participants and research context A dialogue-based ACP educational program was conducted in four regions in Japan for local citizens to discuss the value of their way of life. A total of 66 individuals (mean age = 55.5 ± 17.2 years; 50 women and 16 men) participated in focus group interviews. Ethical considerations This study was approved by the Ethical Review Committee of Tokyo Women’s Medical University (no. 4723) and Kyoto University (no. R2099). Findings Five main themes were extracted: discussing one’s thoughts with others in a considerate manner, reflecting on one’s way of life through others, feeling a sense of connection with others through storytelling, realizing the difficulties of talking about “what if” topics, and turning one’s eyes toward the future through the dialogue. These themes were interrelated and illustrated the complexity of the experience of discussing values. Conclusions The results suggest that dialogue in ACP is useful in clarifying values. They also indicated the need for dealing with the ethical challenges of discussing value and the importance of caring for the interlocutor to have a safe dialogue. In the ACP process, safety in dialogue may improve readiness in ACP, and health practitioners who support ACP need to address the ethical challenges entailing dialogue about values. (shrink)

Music is the carrier through which human beings express their emotions. It can clean up their hearts and seek emotional resonance. The combination of music and artificial intelligence, when music meets artificial intelligence, the mathematical logic part of data and algorithm replaces the image thinking, resulting in automatic music production. The basic principle of music creation is to use artificial intelligence technology to conduct in-depth training on a large number of songs, and then build a database. Then, within a certain (...) period of time, extract a segment from several songs, and then decompose it to form a new melody. The automatic music production is the collision of music and technology. With the flying of code and notes, it creates a different kind of beauty. Music culture is a new field of music application. With its refreshing audio-visual effect, it has made people have a new understanding of music and has become a hot topic in current mass cultural activities. The sound quality characteristics of music culture programs determine the characteristics of simple, fast and efficient design. However, the current audio and video design still stays in the traditional audio and video form design, with low design efficiency, long cycle, high cost and high requirements for designers. In view of the fact that the traditional audio and video design mode in China's music and cultural programs cannot meet the needs of performance programs at present, this paper proposes a design scheme of audio and visual effects of music and cultural programs with intelligent devices as the core, and develops a complete set of audio and visual effects aided design system on this basis. (shrink)

Numerous empirical studies have been conducted to examine first-generation college students, those individuals whose parents have not attended college. Their personality characteristics, cognitive development, academic preparation, and first-year performance have all been topics of research; yet there appears to be little in the literature exploring the motivation of these individuals to seek higher education. There are even fewer studies targeting academic motivation in Hispanic students. The purpose of this study is to conduct a phenomenological examination of the desire to attend (...) college among first generation Hispanic students participating in an academic support program. One-hour taped interviews were conducted with three volunteer participants enrolled in the Student Support Services program at Sul Ross State University. Meaning units and constituents were extracted, and general structures were developed using the Descriptive Phenomenological Method . The phenomenological analysis resulted in two structures that address the effectiveness of academic outreach programming and identify the roles of self-efficacy, successful experiences in high school, a desire for improved socioeconomic status, a need to contribute to the well-being of others, a break with tradition, and the influence of respected role models in facilitating a desire for higher education in first-generation Hispanic college students. (shrink)

Forensic data banks contain biological samples and DNA extracts as well as computerized databases of coded DNA profiles of convicted offenders, arrestees and crime scene samples. When used for investigative and law enforcement purposes, DNA data banks have been successful in providing key investigative leads in hundreds of criminal investigations. A number of these crimes would never have been resolved without use of such data banks. In addition, in some limited number of investigations, the exclusion of known suspects whose DNA (...) profiles are known to be in an offender database can save valuable investigative time.Despite the above benefits, in hundreds of cases DNA samples are never collected and administrative and laboratory logjams delay prompt database searches. Furthermore, hundreds of DNA database matches languish, without any followup by law enforcement or prosecutors. These prevent or delay DNA matches and therefore can leave the public in grave risk of potential harm from recidivistic offenders who otherwise could have been apprehended and convicted if the process functioned more effectively. (shrink)

This paper investigates some delicate tradeoffs between the generality of an algorithmic learning device and the quality of the programs it learns successfully. There are results to the effect that, thanks to small increases in generality of a learning device, the computational complexity of some successfully learned programs is provably unalterably suboptimal. There are also results in which the complexity of successfully learned programs is asymptotically optimal and the learning device is general, but, still thanks to the generality, some of (...) those optimal, learned programs are provably unalterably information deficient—in some cases, deficient as to safe, algorithmic extractability/provability of the fact that they are even approximately optimal. For these results, the safe, algorithmic methods of information extraction will be by proofs in arbitrary, true, computably axiomatizable extensions of Peano Arithmetic. (shrink)

BackgroundChronic airway diseases are prevalent and costly conditions. Interdisciplinary rehabilitation programs that include Acceptance and Commitment-based components could be important to tackle the vicious circle linking progression of the disease, inactivity, and psychopathological symptoms.MethodsA retrospective evaluation of routinely collected data of an interdisciplinary rehabilitation program was performed. The program included group sessions including patient education, breathing exercise, occupational therapy and an ACT-based psychological treatment, and individual sessions of physical therapy. Demographic data, clinical characteristics of the patients and the (...) values of outcome variables before treatment, at discharge, at 3 months, and at 6 months were extracted from medical records. Multiple imputation was employed to address missing data. Linear mixed models were employed to assess changes over time. Multivariable logistic regression was performed to assess predictors of a minimum clinically important change of health status from baseline to the 6-months follow-up.ResultsData from 31 patients with chronic obstructive pulmonary disease and 12 patients with bronchiectasis were extracted. Health status improved from baseline to discharge to the 3 months follow-up, but not to the 6 months follow-up. Anxiety and depression improved across all the time points. Quality of life did not improve over time. Having a worse health status at baseline and fewer depressive symptoms were significantly associated with achieving a minimum clinically important change of health status at 6 months. The effects of the interdisciplinary program were not different for patients with COPD or with bronchiectasis.DiscussionInterdisciplinary programs including ACT-based components are promising treatments for the rehabilitation of patients with chronic airway diseases. (shrink)

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)

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)

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)

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

We will apply the methods developed in the field of ‘proof mining’ to the Bolzano-Weierstraß theorem BW and calibrate the computational contribution of using this theorem in proofs of combinatorial statements. We provide an explicit solution of the Gödel functional interpretation as well as the monotone functional interpretation of BW for the product space Πi ∈ℕ[–ki, ki] . This results in optimal program and bound extraction theorems for proofs based on fixed instances of BW, i.e. for BW applied (...) to fixed sequences in Πi ∈ℕ[–ki, ki]. (shrink)

We study the system IFP of intuitionistic fixed point logic, an extension of intuitionistic first-order logic by strictly positive inductive and coinductive definitions. We define a realizability interpretation of IFP and use it to extract computational content from proofs about abstract structures specified by arbitrary classically true disjunction free formulas. The interpretation is shown to be sound with respect to a domain-theoretic denotational semantics and a corresponding lazy operational semantics of a functional language for extracted programs. We also show how (...) extracted programs can be translated into Haskell. As an application we extract a program converting the signed digit representation of real numbers to infinite Gray code from a proof of inclusion of the corresponding coinductive predicates. (shrink)

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)

From a classical proof that the gcd of natural numbers a1 and a2 is a linear combination of the two, we extract by Gödel's Dialectica interpretation an algorithm computing the coefficients. The proof uses the minimum principle. We show generally how well-founded recursion can be used to Dialectica interpret well-founded induction, which is needed in the proof of the minimum principle. In the special case of the example above it turns out that we obtain a reasonable extracted term, representing an (...) algorithm close to Euclid's. (shrink)

In view of an enhancement of our implementation on the computer, we explore the possibility of an algorithmic optimization of the various proof-theoretic techniques employed by Kohlenbach for the synthesis of new effective uniform bounds out of established qualitative proofs in Numerical Functional Analysis. Concretely, we prove that the method of “colouring” some of the quantifiers as “non-computational” extends well to ε-arithmetization, elimination-of-extensionality and model-interpretation.

This is a tutorial for the Minlog Proof Assistant, version 5.0.

In order to allow the use of axioms in a second‐order system of extracting programs from proofs, we define constant terms, a form of Curry‐Howard terms, whose types are intended to correspond to those axioms. We also define new reduction rules for these new terms so that all consequences of the axioms can be represented. We finally show that the extended Curry‐Howard terms are strongly normalizable.

In programs of acoustic survey, the amount of data collected and the lack of automatic routines for their classification and interpretation can represent a serious obstacle to achieving quick results. To overcome these obstacles, we are proposing an ecosemiotic model of data mining, ecoacoustic event detection and identification, that uses a combination of the acoustic complexity indices and automatically extracts the ecoacoustic events of interest from the sound files. These events may be indicators of environmental functioning at the scale of (...) individual vocal species, the acoustic community, the sound marks, or the soundscape. The EEDI model is represented by three procedural steps: 1) selecting acoustic data according to environmental variables, 2) detecting the events by creating an ecoacoustic event space produced by plotting ACIft and its evenness, 3) identifying events according to the level of correlation between the acoustic signature of the detected events and an ad hoc library of previously identified events. The EEDI procedure can be extensively used in basic and applied research. In particular, EEDI may be used in long-term monitoring programs to assess the effect of climate change on individual vocal species behavior, population, and acoustic community dynamics. The EEDI model can be also used to investigate acoustic human intrusion in natural systems and the effect in urban areas. (shrink)

Work on a computer program called SMILE + IBP (SMart Index Learner Plus Issue-Based Prediction) bridges case-based reasoning and extracting information from texts. The program addresses a technologically challenging task that is also very relevant from a legal viewpoint: to extract information from textual descriptions of the facts of decided cases and apply that information to predict the outcomes of new cases. The program attempts to automatically classify textual descriptions of the facts of legal problems in terms (...) of Factors, a set of classification concepts that capture stereotypical fact patterns that effect the strength of a legal claim, here trade secret misappropriation. Using these classifications, the program can evaluate and explain predictions about a problem’s outcome given a database of previously classified cases. This paper provides an extended example illustrating both functions, prediction by IBP and text classification by SMILE, and reports empirical evaluations of each. While IBP’s results are quite strong, and SMILE’s much weaker, SMILE + IBP still has some success predicting and explaining the outcomes of case scenarios input as texts. It marks the first time to our knowledge that a program can reason automatically about legal case texts. (shrink)