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 25 reviews Date Reviewed 
  A semantic framework for proof evidence
Chihani Z., Miller D., Renaud F.  Journal of Automated Reasoning 59(3): 287-330, 2017. Type: Article

The use of theorem provers as fundamental aids in computer science and software engineering is slowly expanding their reach. The multitude of tools and methods does have a downside: lack of interoperability. It would be nice if, for example, proof...

Feb 6 2018
   Markov chains and Markov decision processes in Isabelle/HOL
Hölzl J.  Journal of Automated Reasoning 59(3): 345-387, 2017. Type: Article

The intermingling of rather different domains can, at times, produce rather interesting results. Here the author explores the intersection of probability theory (in the guise of Markov chains and Markov decision processes) and formal proof (throug...

Jan 11 2018
  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
Display per column
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2018 ThinkLoud, Inc.
Terms of Use
| Privacy Policy