1811 applied aggressively (without considering back-tracking later). |
1811 applied aggressively (without considering back-tracking later). |
1812 Rules declared with ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' are ignored in proof search (the |
1812 Rules declared with ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' are ignored in proof search (the |
1813 single-step \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method still observes these). An |
1813 single-step \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method still observes these). An |
1814 explicit weight annotation may be given as well; otherwise the |
1814 explicit weight annotation may be given as well; otherwise the |
1815 number of rule premises will be taken into account here.% |
1815 number of rule premises will be taken into account here.% |
|
1816 \end{isamarkuptext}% |
|
1817 \isamarkuptrue% |
|
1818 % |
|
1819 \isamarkupsection{Model Elimination and Resolution% |
|
1820 } |
|
1821 \isamarkuptrue% |
|
1822 % |
|
1823 \begin{isamarkuptext}% |
|
1824 \begin{matharray}{rcl} |
|
1825 \indexdef{HOL}{method}{meson}\hypertarget{method.HOL.meson}{\hyperlink{method.HOL.meson}{\mbox{\isa{meson}}}} & : & \isa{method} \\ |
|
1826 \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\ |
|
1827 \end{matharray} |
|
1828 |
|
1829 \begin{railoutput} |
|
1830 \rail@begin{2}{} |
|
1831 \rail@term{\hyperlink{method.HOL.meson}{\mbox{\isa{meson}}}}[] |
|
1832 \rail@bar |
|
1833 \rail@nextbar{1} |
|
1834 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] |
|
1835 \rail@endbar |
|
1836 \rail@end |
|
1837 \rail@begin{5}{} |
|
1838 \rail@term{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}}[] |
|
1839 \rail@bar |
|
1840 \rail@nextbar{1} |
|
1841 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] |
|
1842 \rail@bar |
|
1843 \rail@term{\isa{partial{\isaliteral{5F}{\isacharunderscore}}types}}[] |
|
1844 \rail@nextbar{2} |
|
1845 \rail@term{\isa{full{\isaliteral{5F}{\isacharunderscore}}types}}[] |
|
1846 \rail@nextbar{3} |
|
1847 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}types}}[] |
|
1848 \rail@nextbar{4} |
|
1849 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
|
1850 \rail@endbar |
|
1851 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] |
|
1852 \rail@endbar |
|
1853 \rail@bar |
|
1854 \rail@nextbar{1} |
|
1855 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] |
|
1856 \rail@endbar |
|
1857 \rail@end |
|
1858 \end{railoutput} |
|
1859 |
|
1860 |
|
1861 The \hyperlink{method.HOL.meson}{\mbox{\isa{meson}}} method implements Loveland's model elimination |
|
1862 procedure \cite{loveland-78}. See \verb|~~/src/HOL/ex/Meson_Test.thy| for |
|
1863 examples. |
|
1864 |
|
1865 The \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}} method combines ordered resolution and ordered |
|
1866 paramodulation to find first-order (or mildly higher-order) proofs. The first |
|
1867 optional argument specifies a type encoding; see the Sledgehammer manual |
|
1868 \cite{isabelle-sledgehammer} for details. The \verb|~~/src/HOL/Metis_Examples| directory contains several small theories |
|
1869 developed to a large extent using Metis.% |
1816 \end{isamarkuptext}% |
1870 \end{isamarkuptext}% |
1817 \isamarkuptrue% |
1871 \isamarkuptrue% |
1818 % |
1872 % |
1819 \isamarkupsection{Coherent Logic% |
1873 \isamarkupsection{Coherent Logic% |
1820 } |
1874 } |