Handling Polymorphism in Automated Deduction

DOI10.1007/978-3-540-73595-3_18zbMATH Open1213.68568OpenAlexW1557830359MaRDI QIDQ3608778FDOQ3608778

Authors: Jean-François Couchot, Stéphane Lescuyer 

Publication date: 6 March 2009

Published in: Automated Deduction – CADE-21 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-73595-3_18

Recommendations

• Expressing polymorphic types in a many-sorted language
• Encoding monomorphic and polymorphic types
• Encoding monomorphic and polymorphic types
• One logic to use them all
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism

Mathematics Subject Classification ID

Cited In (7)

• Extending Sledgehammer with SMT solvers
• Extensional higher-order paramodulation in Leo-III
• Expressing polymorphic types in a many-sorted language
• Encoding monomorphic and polymorphic types
• Encoding monomorphic and polymorphic types
• Programming Languages and Systems
• A Polymorphic Vampire

Uses Software

• VAMPIRE
• SMT-LIB
• Yices
• Caduceus

This page was built for publication: Handling Polymorphism in Automated Deduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3608778)