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