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 28 Reviews about "Mechanical Theorem Proving (F.4.1...)": Date Reviewed
  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 as...

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 s...

Mar 9 2017
  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. pr...

Nov 6 2014
  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 p...

Aug 20 2009
  Towards a mechanically checked theory of computation
Moore J. In Logic-based artificial intelligence. Norwell, MA: Kluwer Academic Publishers, 2000.  Type: Book Chapter

This chapter discusses a computational logic for applicative common Lisp (ACL2), which is both a logic, and a theorem prover for that logic. The system can be more generally considered to be in the group of so-called “proof-...

Feb 4 2003
  Automated theorem proving in software engineering
Schumann J., Springer-Verlag New York, Inc., New York, NY, 2001. 228 pp.  Type: Book (9783540679899)

It is obvious that the growing demand for high quality, safety, and security of software systems can be met by rigorous application of formal methods during software design. However, tools for formal methods in general do not provide a...

Jun 5 2002
  Evaluating general purpose automated theorem proving systems
Sutcliffe G., Suttner C. Artificial Intelligence 131(1-2): 39-54, 2001.  Type: Article

The authors discuss the empirical evaluation of general-purpose automated theorem proving systems, and present two schemes for empirical evaluation of fully automatic, sound, possibly incomplete, or bugged automated theorem proving sys...

May 13 2002
  Automated theorem proving: theory and practice
Newborn M., Springer-Verlag New York, Inc., New York, NY, 2001. 231 pp.  Type: Book (9780387950754), Reviews: (2 of 2)

Two very elaborate theorem-proving programs called HERBY and THEO are the focus of this book. Both are included on an accompanying CD-ROM. They are written in clear ANSI C, and are very well documented. Their structures are analyzed in...

Oct 1 2001
  Automated theorem proving: theory and practice
Newborn M., Springer-Verlag New York, Inc., New York, NY, 2001. 231 pp.  Type: Book (9780387950754), Reviews: (1 of 2)

Automated theorem proving (ATP) deals with the development of methods and computer programs that can show that some statement is a logical consequence of a set of statements (the axioms and hypotheses). ATP systems are used in a wide v...

Apr 1 2001
  Robust multi-objective feedback design by quantifier elimination
Dorato P., Yang W., Abdallah C. Journal of Symbolic Computation 24(2): 153-159, 1997.  Type: Article

The research reported here addresses the problem of robust multi-objective feedback design in terms of mathematical logic, using new developments in quantifier elimination theory. As is well known, the general static output feedback st...

Dec 1 1998
Display per page
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2023 ThinkLoud®
Terms of Use
| Privacy Policy