Encoding monomorphic and polymorphic types
From MaRDI portal
Abstract: Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of "cover". The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalised the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes.
Recommendations
Cites work
- A polymorphic intermediate verification language: design and logical encoding
- Automated inference of finite unsatisfiability
- Automated Reasoning
- Basic paramodulation
- Combining superposition, sorts and splitting
- Encoding monomorphic and polymorphic types
- Expressing polymorphic types in a many-sorted language
- Extending Sledgehammer with SMT solvers
- Handling Polymorphism in Automated Deduction
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 53151 (Why is no real title available?)
- scientific article; zbMATH DE number 3467028 (Why is no real title available?)
- Isabelle/HOL. A proof assistant for higher-order logic
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Mechanizing the metatheory of Sledgehammer
- Monotonicity inference for higher-order formulas
- More SPASS with Isabelle
- MPTP 0.2: Design, implementation, and initial experiments
- Schubert's steamroller problem: Formulations and solutions
- Sledgehammer: judgement day
- Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- The TPTP typed first-order form with arithmetic
- Translating higher-order clauses to first-order clauses
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
Cited in
(15)- CoSMed: a confidentiality-verified social media platform
- Encoding types in ML-like languages
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Extensional higher-order paramodulation in Leo-III
- Encoding first order proofs in SMT
- Expressing polymorphic types in a many-sorted language
- Handling Polymorphism in Automated Deduction
- Superposition for lambda-free higher-order logic
- Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic
- Encoding monomorphic and polymorphic types
- Superposition with lambdas
- Superposition with lambdas
- A shallow embedding of pure type systems into first-order logic
- Hammering higher order set theory
- Exploiting instantiations from paramodulation proofs in Isabelle/HOL
Describes a project that uses
Uses Software
This page was built for publication: Encoding monomorphic and polymorphic types
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2974796)
