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
Next revision
Previous revision
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