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









110 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): 205226, 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): 10051026, 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
Truelife 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(34): 193218, 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 Logicbased 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 socalled “proof...

Feb 4 2003 

Automated theorem proving in software engineering Schumann J., SpringerVerlag 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(12): 3954, 2001. Type: Article
The authors discuss the empirical evaluation of generalpurpose 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., SpringerVerlag New York, Inc., New York, NY, 2001. 231 pp. Type: Book (9780387950754), Reviews: (2 of 2)
Two very elaborate theoremproving programs called HERBY and THEO are the focus of this book. Both are included on an accompanying CDROM. 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., SpringerVerlag 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 multiobjective feedback design by quantifier elimination Dorato P., Yang W., Abdallah C. Journal of Symbolic Computation 24(2): 153159, 1997. Type: Article
The research reported here addresses the problem of robust multiobjective 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 





