551 function will be directly applied to as many arguments as possible. Enabling |
551 function will be directly applied to as many arguments as possible. Enabling |
552 this option can sometimes help discover higher-order proofs that otherwise would |
552 this option can sometimes help discover higher-order proofs that otherwise would |
553 not be found. |
553 not be found. |
554 |
554 |
555 \opfalse{full\_types}{partial\_types} |
555 \opfalse{full\_types}{partial\_types} |
556 Specifies whether full-type information is encoded in ATP problems. Enabling |
556 Specifies whether full type information is encoded in ATP problems. Enabling |
557 this option can prevent the discovery of type-incorrect proofs, but it also |
557 this option prevents the discovery of type-incorrect proofs, but it also tends |
558 tends to slow down the ATPs significantly. For historical reasons, the default |
558 to slow down the ATPs significantly. For historical reasons, the default value |
559 value of this option can be overridden using the option ``Sledgehammer: Full |
559 of this option can be overridden using the option ``Sledgehammer: Full Types'' |
560 Types'' from the ``Isabelle'' menu in Proof General. |
560 from the ``Isabelle'' menu in Proof General. |
561 |
561 |
562 \opfalse{full\_types}{partial\_types} |
562 \opfalse{full\_types}{partial\_types} |
563 Specifies whether full-type information is encoded in ATP problems. Enabling |
563 Specifies whether full-type information is encoded in ATP problems. Enabling |
564 this option can prevent the discovery of type-incorrect proofs, but it also |
564 this option can prevent the discovery of type-incorrect proofs, but it also |
565 tends to slow down the ATPs significantly. For historical reasons, the default |
565 tends to slow down the ATPs significantly. For historical reasons, the default |
603 \item[$\bullet$] \textbf{\textit{mangled\_tags}:} Similar to |
603 \item[$\bullet$] \textbf{\textit{mangled\_tags}:} Similar to |
604 \textit{mono\_tags}, but types are mangled in constant names instead of being |
604 \textit{mono\_tags}, but types are mangled in constant names instead of being |
605 supplied as ground term arguments. The binary function |
605 supplied as ground term arguments. The binary function |
606 $\mathit{type\_info\/}(\tau, t)$ becomes a unary function |
606 $\mathit{type\_info\/}(\tau, t)$ becomes a unary function |
607 $\mathit{type\_info\_}\tau(t)$. |
607 $\mathit{type\_info\_}\tau(t)$. |
|
608 |
|
609 \item[$\bullet$] |
|
610 \textbf{% |
|
611 \textit{preds}?, |
|
612 \textit{mono\_preds}?, |
|
613 \textit{mangled\_preds}?, \\ |
|
614 \textit{tags}?, |
|
615 \textit{mono\_tags}?, |
|
616 \textit{mangled\_tags}?:} \\ |
|
617 The type systems \textit{preds}, \textit{mono\_preds}, \textit{mangled\_preds}, |
|
618 \textit{tags}, \textit{mono\_tags}, and \textit{mangled\_tags} are fully typed |
|
619 and virtually sound---i.e., except for pathological cases, all found proofs are |
|
620 type-correct. For each of these, Sledgehammer also provides a just-as-sound |
|
621 partially typed variant identified by a question mark (?)\ that detects and |
|
622 erases monotonic types (notably infinite types). |
608 |
623 |
609 \item[$\bullet$] |
624 \item[$\bullet$] |
610 \textbf{% |
625 \textbf{% |
611 \textit{preds}!, |
626 \textit{preds}!, |
612 \textit{mono\_preds}!, |
627 \textit{mono\_preds}!, |
613 \textit{mangled\_preds}!, \\ |
628 \textit{mangled\_preds}!, \\ |
614 \textit{tags}!, |
629 \textit{tags}!, |
615 \textit{mono\_tags}!, |
630 \textit{mono\_tags}!, |
616 \textit{mangled\_tags}!:} \\ |
631 \textit{mangled\_tags}!:} \\ |
617 The type systems \textit{preds}, \textit{mono\_preds}, \textit{mangled\_preds}, |
632 If the question mark (?)\ is replaced by an exclamation mark (!),\ the |
618 \textit{tags}, \textit{mono\_tags}, and \textit{mangled\_tags} are fully typed |
633 translation erases all types except those that are clearly finite (e.g., |
619 and virtually sound. For each of these, Sledgehammer also provides a mildly |
634 \textit{bool}). This encoding is unsound. |
620 unsound variant identified by an exclamation mark (!)\ that types only finite |
|
621 (and hence especially dangerous) types. |
|
622 |
|
623 \item[$\bullet$] |
|
624 \textbf{% |
|
625 \textit{preds}?, |
|
626 \textit{mono\_preds}?, |
|
627 \textit{mangled\_preds}?, \\ |
|
628 \textit{tags}?, |
|
629 \textit{mono\_tags}?, |
|
630 \textit{mangled\_tags}?:} \\ |
|
631 If the exclamation mark (!)\ is replaced by an question mark (?),\ the type |
|
632 systems type only nonmonotonic (and hence especially dangerous) types. Not |
|
633 implemented yet. |
|
634 |
635 |
635 \item[$\bullet$] \textbf{\textit{const\_args}:} |
636 \item[$\bullet$] \textbf{\textit{const\_args}:} |
636 Constants are annotated with their types, supplied as extra arguments, to |
637 Like for the other sound encodings, constants are annotated with their types to |
637 resolve overloading. Variables are unbounded. |
638 resolve overloading, but otherwise no type information is encoded. This encoding |
|
639 is hence less sound than the exclamation mark (!)\ variants described above. |
638 |
640 |
639 \item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to |
641 \item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to |
640 the ATP. Types are simply erased. |
642 the ATP. Types are simply erased. |
641 |
643 |
642 \item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled, |
644 \item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled, |