Please use this identifier to cite or link to this item: http://hdl.handle.net/123456789/13603
Title: SPECIF'YCATIORJ AND VERIFICATION OF BLOCK WORLD DOMAIN IiV COQ
Authors: Tanwar, Gajraj Singh
Keywords: ELECTRONICS AND COMPUTER ENGINEERING
BLOCK WORLD
COMPUTER PROGRAM
LOGIC
Issue Date: 2012
Abstract: Automated Theorem Proving (ATP) or Automated Deduction, currently the most well-developed subfield of Automated Reasoning (AR), is the proving of mathematical theorems by a computer program. Depending on the underlying logic, the problem of deciding the validity of a formula varies from trivial to impossible. A simpler, but related, problem is proof verification, where an existing proof for a theorem is certified valid. For this, it is generally required that each individual proof step can be verified by a primitive recursive function or program, and hence the problem is always decidable. Interactive Theorem Prover requires a human user to give hints to the system. Depending on the degree of automation, the prover can essentially be reduced to a proof checker, with the user providing the proof in a formal way, or significant proof tasks can be performed automatically. Interactive prover's are used for a variety of tasks, but even fully automatic systems have proven a number of interesting and hard theorems. There are several types of theorem prover like Coq, which have its own specification languages, in which we can specify a system in a logical form with the help of predicates and write the theorem related to the properties of the system. These can be verified with the help of proof assistant.
URI: http://hdl.handle.net/123456789/13603
Other Identifiers: M.Tech
Appears in Collections:MASTERS' DISSERTATIONS (E & C)

Files in This Item:
File Description SizeFormat 
ECE G21479.pdf1.09 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.