Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav08:axioms_of_hol [2008/05/28 03:06]
vkuncak
sav08:axioms_of_hol [2015/04/21 17:30] (current)
Line 1: Line 1:
-====== Axioms of Classical HOL ======+====== Axioms ​and Inference Rules of Classical HOL ======
  
 Axiom system that is sound (but necessarily incomplete with respect to standard semantics) is the following: Axiom system that is sound (but necessarily incomplete with respect to standard semantics) is the following:
Line 8: Line 8:
  
 Inference rule: Inference rule:
-\[+\begin{equation*}
    ​\frac{C\ \ ; \ \ A=B}    ​\frac{C\ \ ; \ \ A=B}
         {C[A:=B]}         {C[A:=B]}
-\]+\end{equation*}
 which replaces one occurrence of $A$ in $C$ with $B$ (we cannot replace variables under $\lambda$) which replaces one occurrence of $A$ in $C$ with $B$ (we cannot replace variables under $\lambda$)
 
sav08/axioms_of_hol.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice