797 down the ATP slightly. This option is implicitly enabled for automatic runs. For |
797 down the ATP slightly. This option is implicitly enabled for automatic runs. For |
798 historical reasons, the default value of this option can be overridden using the |
798 historical reasons, the default value of this option can be overridden using the |
799 option ``Sledgehammer: Full Types'' from the ``Isabelle'' menu in Proof General. |
799 option ``Sledgehammer: Full Types'' from the ``Isabelle'' menu in Proof General. |
800 |
800 |
801 \opdefault{type\_sys}{string}{smart} |
801 \opdefault{type\_sys}{string}{smart} |
802 Specifies the type system to use in ATP problems. The option can take the |
802 Specifies the type system to use in ATP problems. Some of the type systems are |
803 following values: |
803 unsound, meaning that they can give rise to spurious proofs (unreconstructible |
804 |
804 using Metis). The supported type systems are listed below, with an indication of |
805 \begin{enum} |
805 their soundness in parentheses: |
806 \item[$\bullet$] \textbf{\textit{poly\_preds}:} Types are encoded using a predicate |
806 |
807 $\mathit{has\_type\/}(\tau, t)$ that restricts the range of bound variables. |
807 \begin{enum} |
808 Constants are annotated with their types, supplied as extra arguments, to |
808 \item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is |
809 resolve overloading. |
809 supplied to the ATP. Types are simply erased. |
810 |
810 |
811 \item[$\bullet$] \textbf{\textit{poly\_tags}:} Each term and subterm is tagged with |
811 \item[$\bullet$] \textbf{\textit{poly\_preds} (sound):} Types are encoded using |
812 its type using a function $\mathit{type\_info\/}(\tau, t)$. |
812 a predicate \textit{has\_\allowbreak type\/}$(\tau, t)$ that restricts the range |
813 |
813 of bound variables. Constants are annotated with their types, supplied as extra |
814 \item[$\bullet$] \textbf{\textit{poly\_args}:} |
814 arguments, to resolve overloading. |
815 Like for the other sound encodings, constants are annotated with their types to |
815 |
|
816 \item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is |
|
817 tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$. |
|
818 |
|
819 \item[$\bullet$] \textbf{\textit{poly\_args} (unsound):} |
|
820 Like for \textit{poly\_preds} constants are annotated with their types to |
816 resolve overloading, but otherwise no type information is encoded. |
821 resolve overloading, but otherwise no type information is encoded. |
817 |
|
818 \item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to |
|
819 the ATP. Types are simply erased. |
|
820 |
822 |
821 \item[$\bullet$] |
823 \item[$\bullet$] |
822 \textbf{% |
824 \textbf{% |
823 \textit{mono\_preds}, |
825 \textit{mono\_preds}, \textit{mono\_tags} (sound); |
824 \textit{mono\_tags}, |
826 \textit{mono\_args} (unsound):} \\ |
825 \textit{mono\_args}:} \\ |
|
826 Similar to \textit{poly\_preds}, \textit{poly\_tags}, and \textit{poly\_args}, |
827 Similar to \textit{poly\_preds}, \textit{poly\_tags}, and \textit{poly\_args}, |
827 respectively, but the problem is additionally monomorphized, meaning that type |
828 respectively, but the problem is additionally monomorphized, meaning that type |
828 variables are instantiated with heuristically chosen ground types. |
829 variables are instantiated with heuristically chosen ground types. |
829 Monomorphization can simplify reasoning but also leads to larger fact bases, |
830 Monomorphization can simplify reasoning but also leads to larger fact bases, |
830 which can slow down the ATPs. |
831 which can slow down the ATPs. |
831 |
832 |
832 \item[$\bullet$] \textbf{\textit{simple}:} Use the prover's support for simply |
|
833 typed first-order logic if available; otherwise, fall back on |
|
834 \textit{mangled\_preds}. The problem is monomorphized. |
|
835 |
|
836 \item[$\bullet$] |
833 \item[$\bullet$] |
837 \textbf{% |
834 \textbf{% |
838 \textit{mangled\_preds}, |
835 \textit{mangled\_preds}, |
839 \textit{mangled\_tags}, |
836 \textit{mangled\_tags} (sound); \\ |
840 \textit{mangled\_args}:} \\ |
837 \textit{mangled\_args} (unsound):} \\ |
841 Similar to |
838 Similar to |
842 \textit{mono\_preds}, \textit{mono\_tags}, and \textit{mono\_args}, |
839 \textit{mono\_preds}, \textit{mono\_tags}, and \textit{mono\_args}, |
843 respectively but types are mangled in constant names instead of being supplied |
840 respectively but types are mangled in constant names instead of being supplied |
844 as ground term arguments. The binary predicate $\mathit{has\_type\/}(\tau, t)$ |
841 as ground term arguments. The binary predicate $\mathit{has\_type\/}(\tau, t)$ |
845 becomes a unary predicate $\mathit{has\_type\_}\tau(t)$, and the binary function |
842 becomes a unary predicate $\mathit{has\_type\_}\tau(t)$, and the binary function |
846 $\mathit{type\_info\/}(\tau, t)$ becomes a unary function |
843 $\mathit{type\_info\/}(\tau, t)$ becomes a unary function |
847 $\mathit{type\_info\_}\tau(t)$. |
844 $\mathit{type\_info\_}\tau(t)$. |
848 |
845 |
|
846 \item[$\bullet$] \textbf{\textit{simple} (sound):} Use the prover's support for |
|
847 simply typed first-order logic if available; otherwise, fall back on |
|
848 \textit{mangled\_preds}. The problem is monomorphized. |
|
849 |
849 \item[$\bullet$] |
850 \item[$\bullet$] |
850 \textbf{% |
851 \textbf{% |
851 \textit{mono\_preds}?, \textit{mono\_tags}?, \textit{simple}?, \\ |
852 \textit{poly\_preds}?, \textit{poly\_tags}?, \textit{mono\_preds}?, \textit{mono\_tags}?, \\ |
852 \textit{mangled\_preds}?, \textit{mangled\_tags}?:} \\ |
853 \textit{mangled\_preds}?, \textit{mangled\_tags}?, \textit{simple}? (quasi-sound):} \\ |
853 The type systems \textit{mono\_preds}, \textit{mono\_tags}, \textit{simple}, |
854 The type systems \textit{poly\_preds}, \textit{poly\_tags}, |
854 \textit{mangled\_preds}, and \textit{mangled\_tags} are fully typed and |
855 \textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds}, |
855 virtually sound---except for pathological cases, all found proofs are |
856 \textit{mangled\_tags}, and \textit{simple} are fully typed and sound. For each |
856 type-correct. For each of these, Sledgehammer also provides a lighter (but |
857 of these, Sledgehammer also provides a lighter, virtually sound variant |
857 virtually sound) variant identified by a question mark (`{?}')\ that detects and |
858 identified by a question mark (`{?}')\ that detects and erases monotonic types, |
858 erases monotonic types, notably infinite types. (For \textit{simple}, the types |
859 notably infinite types. (For \textit{simple}, the types are not actually erased |
859 are not actually erased but rather replaced by a shared uniform type of |
860 but rather replaced by a shared uniform type of individuals.) |
860 individuals.) |
|
861 |
861 |
862 \item[$\bullet$] |
862 \item[$\bullet$] |
863 \textbf{% |
863 \textbf{% |
864 \textit{poly\_tags}!, \textit{mono\_preds}!, \textit{mono\_tags}!, \\ |
864 \textit{poly\_preds}!, \textit{poly\_tags}!, \textit{mono\_preds}!, \textit{mono\_tags}!, \\ |
865 \textit{simple}!, \textit{mangled\_preds}!, \textit{mangled\_tags}!:} \\ |
865 \textit{mangled\_preds}!, \textit{mangled\_tags}!, \textit{simple}! \\ |
|
866 (mildly unsound):} \\ |
866 The type systems \textit{poly\_preds}, \textit{poly\_tags}, |
867 The type systems \textit{poly\_preds}, \textit{poly\_tags}, |
867 \textit{mono\_preds}, \textit{mono\_tags}, \textit{simple}, |
868 \textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds}, |
868 \textit{mangled\_preds}, and \textit{mangled\_tags} also admit a somewhat |
869 \textit{mangled\_tags}, and \textit{simple} also admit a mildly unsound (but |
869 unsound (but very efficient) variant identified by an exclamation mark (`{!}') |
870 very efficient) variant identified by an exclamation mark (`{!}') that detects |
870 that detects and erases erases all types except those that are clearly finite |
871 and erases erases all types except those that are clearly finite (e.g., |
871 (e.g., \textit{bool}). (For \textit{simple}, the types are not actually erased |
872 \textit{bool}). (For \textit{simple}, the types are not actually erased but |
872 but rather replaced by a shared uniform type of individuals.) |
873 rather replaced by a shared uniform type of individuals.) |
873 |
874 |
874 \item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled, |
875 \item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled, |
875 uses a fully typed, virtually sound encoding; otherwise, uses any encoding. The |
876 uses a sound or virtually sound encoding; otherwise, uses any encoding. The actual |
876 actual encoding used depends on the ATP and should be the most efficient for |
877 encoding used depends on the ATP and should be the most efficient for that ATP. |
877 that ATP. |
|
878 \end{enum} |
878 \end{enum} |
879 |
879 |
880 In addition, all the \textit{preds} and \textit{tags} type systems are available |
880 In addition, all the \textit{preds} and \textit{tags} type systems are available |
881 in two variants, a lightweight and a heavyweight variant. The lightweight |
881 in two variants, a lightweight and a heavyweight variant. The lightweight |
882 variants are generally more efficient and are the default; the heavyweight |
882 variants are generally more efficient and are the default; the heavyweight |