SPECIF'YCATIORJ AND VERIFICATION OF BLOCK WORLD DOMAIN IiV COQ

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.