Evidence Algorithm and Processing Formalized Mathematical Texts

The goal of a research programme Evidence Algorithm is a development of an open system of automated proving that is able to accumulate mathematical knowledge and to prove theorems in a context of a self-contained mathematical text. By now, the first version of such a system called a System for Automated Deduction, SAD, is implemented in software. The system SAD possesses the following main features: mathematical texts are formalized using a specific formal language that is close to a natural language of mathematical publications; a proof search is based on special sequent-type calculi formalizing natural reasoning style, such as application of definitions and auxiliary propositions. These calculi also admit a separation of equality handling from deduction that gives an opportunity to integrate logical reasoning with symbolic calculation.

Meeting the Standards: An Analysis of Eight Grade Educational Assesment Test Scores in Maine

This paper examines the impact of socioeconomic factors on eighth grade achievement test scores in the face of federal and state initiatives for educational reform in Maine. We use student-level data over a five year period to provide a framework for understanding the policy implications of these initiatives. We model performance on standardized tests using a seemingly unrelated regressions approach and then determine the likelihood of meeting the standards defined by the adequate yearly progress requirements of the No Child Left Behind Act and Maine Learning Results initiatives. Our results indicate that the key factors influencing a student’s test scores include the education of a student’s parents, special services received for learning disabilities, and alternative measures of academic achievement.