Home
This Title All WIREs
WIREs RSS Feed
How to cite this WIREs title:
WIREs Cogn Sci
Impact Factor: 3.175

Automated theorem proving

Full article on Wiley Online Library:   HTML PDF

Can't access this content? Tell your librarian.

Automated theorem proving is the use of computers to prove or disprove mathematical or logical statements. Such statements can express properties of hardware or software systems, or facts about the world that are relevant for applications such as natural language processing and planning. A brief introduction to propositional and first‐order logic is given, along with some of the main methods of automated theorem proving in these logics. These methods of theorem proving include resolution, Davis and Putnam‐style approaches, and others. Methods for handling the equality axioms are also presented. Methods of theorem proving in propositional logic are presented first, and then methods for first‐order logic. WIREs Cogn Sci 2014, 5:115–128. doi: 10.1002/wcs.1269 This article is categorized under: Computer Science > Artificial Intelligence Philosophy > Artificial Intelligence Philosophy > Knowledge and Belief
A semantic tree.
[ Normal View | Magnified View ]

Browse by Topic

Computer Science > Artificial Intelligence
Philosophy > Knowledge and Belief
Philosophy > Artificial Intelligence

Access to this WIREs title is by subscription only.

Recommend to Your
Librarian Now!

The latest WIREs articles in your inbox

Sign Up for Article Alerts