Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sav08:complete_recursive_axiomatizations [2008/04/06 16:59]
vkuncak
sav08:complete_recursive_axiomatizations [2009/05/16 10:47] (current)
vkuncak
Line 8: Line 8:
 **Proof.**++++| **Proof.**++++|
 Suppose $Ax$ is a complete recursive axiomatization. ​ There are two cases, depending on whether $Ax$ is consistent. Suppose $Ax$ is a complete recursive axiomatization. ​ There are two cases, depending on whether $Ax$ is consistent.
-  * **Case 1):** The set $Ax$ is inconsistent,​ that is, there are not models for $Ax$.  Then $Conseq(Ax)$ is the set of all first-order sentences and there is a trivial algorithm for checking whether $F \in Conseq(Ax)$:​ always return true.+  * **Case 1):** The set $Ax$ is inconsistent,​ that is, there are no models for $Ax$.  Then $Conseq(Ax)$ is the set of all first-order sentences and there is a trivial algorithm for checking whether $F \in Conseq(Ax)$:​ always return true.
   * **Case 2):** The set $Ax$ is consistent. ​ Given $F$, to check whether $F \in Conseq(Ax)$ we run in parallel two complete theorem provers (which exist by [[lecture10|Herbrand theorem]]), the first one trying to prove the formula $F$, the second one trying to prove the formula $\lnot F$; the procedure terminates if any of these theorem provers succeed (the theorem provers simultaneously searches for longer and longer proofs from a larger and larger finite subsets of $Ax$). We show that this is an algorithm that decides $F \in Conseq(Ax)$.   * **Case 2):** The set $Ax$ is consistent. ​ Given $F$, to check whether $F \in Conseq(Ax)$ we run in parallel two complete theorem provers (which exist by [[lecture10|Herbrand theorem]]), the first one trying to prove the formula $F$, the second one trying to prove the formula $\lnot F$; the procedure terminates if any of these theorem provers succeed (the theorem provers simultaneously searches for longer and longer proofs from a larger and larger finite subsets of $Ax$). We show that this is an algorithm that decides $F \in Conseq(Ax)$.
     * Because either $F \in Conseq(Ax)$ or $(\lnot F) \in Conseq(Ax)$,​ and theorem provers are complete, one of these theorem provers will eventually halt.  The procedure is therefore an algorithm.     * Because either $F \in Conseq(Ax)$ or $(\lnot F) \in Conseq(Ax)$,​ and theorem provers are complete, one of these theorem provers will eventually halt.  The procedure is therefore an algorithm.
 
sav08/complete_recursive_axiomatizations.txt · Last modified: 2009/05/16 10:47 by vkuncak
 
© EPFL 2018 - Legal notice