Encoding Monomorphic and Polymorphic Types

DOI10.2168/LMCS-12(4:13)2016zbMath1445.68327arXiv1609.08916MaRDI QIDQ2974796

Andrei Popescu, Jasmin Christian Blanchette, Sascha Böhme, Nicholas Smallbone

Publication date: 11 April 2017

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1609.08916

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

CoSMed: a confidentiality-verified social media platform, Extensional higher-order paramodulation in Leo-III, Unnamed Item, First-order automated reasoning with theories: when deduction modulo theory meets practice, Superposition with lambdas, Superposition with lambdas

Uses Software

• Isabelle/HOL
• MPTP 0.2
• VAMPIRE
• TPTP
• Why3
• Metis_
• z3
• Sledgehammer
• Boogie
• E Theorem Prover
• Jahob

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automated inference of finite unsatisfiability
• Monotonicity inference for higher-order formulas
• MPTP 0.2: Design, implementation, and initial experiments
• Schubert's steamroller problem: Formulations and solutions
• Isabelle/HOL. A proof assistant for higher-order logic
• Basic paramodulation
• Extending Sledgehammer with SMT solvers
• Translating higher-order clauses to first-order clauses
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Mechanizing the Metatheory of Sledgehammer
• The TPTP Typed First-Order Form with Arithmetic
• More SPASS with Isabelle
• Expressing Polymorphic Types in a Many-Sorted Language
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• A Polymorphic Intermediate Verification Language: Design and Logical Encoding
• Handling Polymorphism in Automated Deduction
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
• Sort It Out with Monotonicity
• Automated Reasoning
• Encoding Monomorphic and Polymorphic Types
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• Sledgehammer: Judgement Day