Please use this identifier to cite or link to this item: http://hdl.handle.net/2445/109943
Title: Automated theorem proving
Author: Montserrat Armstrong, Miquel
Director: Martínez Alonso, Juan Carlos
Keywords: Lògica
Tesis
Lògica de primer ordre
Programació lògica
PROLOG (Llenguatges de programació)
Logic
Theses
First-order logic
Logic programming
Prolog (Computer program language)
Issue Date: 27-Jun-2016
Abstract: Automated Theorem Proving is an area in mathematical logic and computer science dedicated to the production of theorem proofs by algorithmical means, and is of great use in many fields such as some areas of mathematics, artificial intelligence, software verification, hardware verification or declarative programming. The aim of the first part of this work is to present Herbrand’s theory and the Resolution Method for the first order logic. In the second part we show one of the many applications of the Resolution Method: the Prolog programming language, which is a useful tool for the resolution of problems in the NP class.
Note: Treballs Finals de Grau de Matemàtiques, Facultat de Matemàtiques, Universitat de Barcelona, Any: 2016, Director: Juan Carlos Martínez Alonso
URI: http://hdl.handle.net/2445/109943
Appears in Collections:Treballs Finals de Grau (TFG) - Matemàtiques

Files in This Item:
File Description SizeFormat 
memoria.pdfMemòria316.54 kBAdobe PDFView/Open


This item is licensed under a Creative Commons License Creative Commons