Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Browse by topic Browse by titles Authors Reviewers Browse by issue Browse Help
Journal of Automated Reasoning
Kluwer Academic Publishers
  1-10 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): 343-365, 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 higher-order abstract syntax representations
Felty A., Momigliano A., Pientka B.  Journal of Automated Reasoning 55(4): 307-372, 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): 199-210, 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): 39-59, 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 first-order theorem proving
Bridge J., Holden S., Paulson L.  Journal of Automated Reasoning 53(2): 141-172, 2014. Type: Article, Reviews: (2 of 2)

Bridge and colleagues have developed a methodology of machine learning for theorem proving that uses real-valued 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 first-order theorem proving
Bridge J., Holden S., Paulson L.  Journal of Automated Reasoning 53(2): 141-172, 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, high-assurance design and verification of systems. Humans certainly need theorem provers’ help for many types of today’s...

Jun 29 2015
  On the fine-structure of regular algebra
Foster S., Struth G.  Journal of Automated Reasoning 54(2): 165-197, 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): 173-190, 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): 229-241, 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): 185-207, 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 per column
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2017 ThinkLoud, Inc.
Terms of Use
| Privacy Policy