Search
w/in this Title
for Titles
All Reviews
Journal of Automated Reasoning
Kluwer Academic Publishers
Options:
Date Reviewed
Title
Author
Publisher
Published Date
Descending Order
Ascending Order
110 of 23 reviews
Date Reviewed
Completeness and decidability results for CTL in constructive type theory
Doczkal C., Smolka G. Journal of Automated Reasoning 56(3): 343365, 2016. Type: Article
The following sentence from the rather demanding introduction to this quite demanding paper reveals common ground between us users of formal methods and the expert authors of this paper: “Given the practical importance of CTL [computation tr...
Jul 15 2016
The next 700 challenge problems for reasoning with higherorder abstract syntax representations
Felty A., Momigliano A., Pientka B. Journal of Automated Reasoning 55(4): 307372, 2015. Type: Article
Understanding how to reason about programs took a great leap forward with the POPLmark challenge [1], which set out some benchmarks for measuring many aspects of programming languages that are difficult to formalize. Chief among them is variable b...
Jun 15 2016
Reconsidering pairs and functions as sets
Brown C. Journal of Automated Reasoning 55(3): 199210, 2015. Type: Article
In set theory, a pair (
x
,
y
) is normally described using Kuratowski’s representation {{
x
},{
x
,
y
}}. The set of all the pairs (
x
,
Dec 8 2015
Automated theorem proving in GeoGebra: current achievements
Botana F., Hohenwarter M., Janicic P., Kovács Z., Petrovi
I., Recio T., Weitzhofer S. Journal of Automated Reasoning 55(1): 3959, 2015. Type: Article
Mathematics has been for a long time, and is still today, a difficult subject for many students. Teachers continuously look for ways to help students understand mathematical theorems, rules, and the relation between algebra and geometry. Besides m...
Oct 6 2015
Machine learning for firstorder theorem proving
Bridge J., Holden S., Paulson L. Journal of Automated Reasoning 53(2): 141172, 2014. Type: Article, Reviews: (2 of 2)
Bridge and colleagues have developed a methodology of machine learning for theorem proving that uses realvalued features of the problem at hand and determines in a rigorous manner and with fewer preconceptions the possible connections between fea...
Jul 22 2015
Machine learning for firstorder theorem proving
Bridge J., Holden S., Paulson L. Journal of Automated Reasoning 53(2): 141172, 2014. Type: Article, Reviews: (1 of 2)
Automatic theorem provers, which today are no longer new things, can be said to be powerful tools in, for example, highassurance design and verification of systems. Humans certainly need theorem provers’ help for many types of today’s...
Jun 29 2015
On the finestructure of regular algebra
Foster S., Struth G. Journal of Automated Reasoning 54(2): 165197, 2015. Type: Article
Although it is dangerous to generalize from a single example, it’s instructive to look at Foster and Struth’s paper as giving us a snapshot of the state of the art in automating ordinary reasoning. First, let’s look at the partic...
May 28 2015
The HOL light theory of Euclidean space
Harrison J. Journal of Automated Reasoning 50(2): 173190, 2013. Type: Article
A formal approach to logic and reasoning initiated by Frege in the late 19th and early 20th centuries marked a step function in the evolution of the subject. In the following decades, the foundations of modern mathematics and logic were cemented b...
Apr 22 2013
ATP and presentation service for Mizar formalizations
Urban J., Rudnicki P., Sutcliffe G. Journal of Automated Reasoning 50(2): 229241, 2013. Type: Article
Mizar is a formal language used to write mathematical definitions and proofs that are as close as possible to vernacular. One can profit from Mizar by using it as: an integrated library (linked within itself) containing proofs generated through th...
Apr 18 2013
A canonical locally named representation of binding
Pollack R., Sato M., Ricciotti W. Journal of Automated Reasoning 49(2): 185207, 2012. Type: Article
Variables underpin mathematics and logic, appearing in algebraic equations, integrals, and quantified formulas, to give three examples. In an algebraic equation, there is usually implicit universal quantification. The variables range over all (sui...
Dec 18 2012
Display
5
10
15
25
50
100
per column
Reproduction in whole or in part without permission is prohibited. Copyright © 20002017 ThinkLoud, Inc.
Terms of Use

Privacy Policy