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
  Browse All Reviews > Theory Of Computation (F) > Mathematical Logic And Formal Languages (F.4) > Mathematical Logic (F.4.1) > Mechanical Theorem Proving (F.4.1...)  
  1-10 of 95 Reviews about "Mechanical Theorem Proving (F.4.1...)": Date Reviewed
  Fundamental proof methods in computer science: a computer-based approach
Arkoudas K., Musser D.,  MIT Press, Cambridge, MA, 2017.Type: Book (9780262035538)

An introduction to proof methods in computer science (CS), this book is set apart from other by its reliance on an interactive theorem prover (called Athena) to achieve the task....

Sep 21 2017
  A theorem about computationalism and "absolute" truth
Charlesworth A.  Minds and Machines 26(3): 205-226, 2016. Type: Article

Is logical inconsistency (or fallibility) an inherent advantage of the human mind over computers? Does computing need to be logical? Minsky, in a quote reproduced in the paper, thought that, “There’s no reason to assume ... that either...

Jun 2 2017
  Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
Aransay J., Divasón J.  Formal Aspects of Computing 28(6): 1005-1026, 2016. Type: Article

Formalization is rapidly evolving from being highly desirable but thought too difficult to be realistic, to being quite feasible and well on its way to being expected. The raw technology of theorem provers certainly is ready. What is still evolvin...

Mar 9 2017
  Synthesis of list algorithms by mechanical proving
Drmnesc I., Jebelean T.  Journal of Symbolic Computation 69(C): 61-92, 2015. Type: Article

Program synthesis via extraction of programs from constructive proofs is now very well established, with a large literature base. There are still quite a few hurdles to overcome, but the meta-theory has been in place for quite some time now....

Jan 11 2016
  The little prover
Friedman D., Eastlund C.,  The MIT Press, Cambridge, MA, 2015. 248 pp. Type: Book (978-0-262527-95-8)

The goal of this book is to teach readers how to prove that recursive Lisp programs are correct. The method used is based on principles from mathematical logic; it involves identifying basic axioms, theorems, and rules of text transformation, and ...

Dec 9 2015
  A certified reduction strategy for homological image processing
Poza M., Domínguez C., Heras J., Rubio J.  ACM Transactions on Computational Logic 15(3): Article No. 23, 2014. Type: Article

True-life biomedical images, such as the synapses of neurons, are too large and onerous to process. How should the data structures of huge digital images be reliably condensed without losing their homological properties? Poza et al. propose a spec...

Nov 6 2014
  A framework for testing first-order logic axioms in program verification
Ahn K., Denney E.  Software Quality Journal 21(1): 159-200, 2013. Type: Article

As model-driven code generators have increased in capability and in performance, so too has their use in mission-critical software development. One benefit of auto-generated code over handcrafted, individually created source code is that it is sim...

Jun 4 2014
  Flow logic for process calculi
Nielson H., Nielson F., Pilegaard H.  ACM Computing Surveys 44(1): 1-39, 2012. Type: Article

Nielson et al. present an approach using flow logic to represent programming notations in process calculi. Flow logic is usually used in static analysis for language paradigms, including imperative, functional, and concurrent features. The lambda ...

May 30 2012
  Weyl’s predicative classical mathematics as a logic-enriched type theory
Adams R., Luo Z.  ACM Transactions on Computational Logic 11(2): 1-29, 2010. Type: Article

Given proof-assistant builders’ renewed interest in foundational issues, revisiting Hermann Weyl’s classic text [1] is a worthy endeavor. Unfortunately, this paper greatly disappoints....

May 28 2010
  Data compression for proof replay
Amjad H.  Journal of Automated Reasoning 41(3-4): 193-218, 2008. Type: Article

Interactive theorem provers suffer from a disadvantage implied by the name: in the proof of a nontrivial theorem, manual guidance by the user is often required. By contrast, Boolean satisfiability (SAT) solvers are powerful tools for propositional...

Aug 20 2009
Display per page
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2022 ThinkLoud, Inc.
Terms of Use
| Privacy Policy