Handling Polymorphism in Automated Deduction

DOI10.1007/978-3-540-73595-3_18MaRDI QIDQ3608778zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Describes a project that uses

Uses Software

• Caduceus
• Yices
• SMT-LIB
• VAMPIRE

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)