Translating higher-order clauses to first-order clauses

DOI10.1007/s10817-007-9085-yzbMath1203.68188DBLPjournals/jar/MengP08OpenAlexW1979623128WikidataQ57382631 ScholiaQ57382631MaRDI QIDQ2471742

Jia Meng, Lawrence Charles Paulson

Publication date: 18 February 2008

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-007-9085-y

zbMATH Keywords

Higher-order logicFirst-order logicClause translationInteractive theorem provers

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Related Items (37)

Automating change of representation for proofs in discrete mathematics (extended version) ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ Automatic Proof and Disproof in Isabelle/HOL ⋮ Expressing Polymorphic Types in a Many-Sorted Language ⋮ From informal to formal proofs in Euclidean geometry ⋮ Semantic subtyping with an SMT solver ⋮ Hammer for Coq: automation for dependent type theory ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Unnamed Item ⋮ Making PVS accessible to generic services by interpretation in a universal format ⋮ Encoding Monomorphic and Polymorphic Types ⋮ Relational characterisations of paths ⋮ Unnamed Item ⋮ MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ MaLeCoP Machine Learning Connection Prover ⋮ Sledgehammer: Judgement Day ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ Extending Sledgehammer with SMT Solvers ⋮ Sort It Out with Monotonicity ⋮ A Foundational View on Integration Problems ⋮ Superposition with lambdas ⋮ Superposition with lambdas ⋮ Limited second-order functionality in a first-order setting ⋮ Validating QBF Validity in HOL4 ⋮ Proving Valid Quantified Boolean Formulas in HOL Light ⋮ Extending SMT solvers to higher-order logic ⋮ Restricted combinatory unification ⋮ GRUNGE: a grand unified ATP challenge ⋮ ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) ⋮ Mining State-Based Models from Proof Corpora ⋮ A FORMAL SYSTEM FOR EUCLID’SELEMENTS ⋮ A Knuth-Bendix-like ordering for orienting combinator equations ⋮ A combinator-based superposition calculus for higher-order logic ⋮ Extending Sledgehammer with SMT solvers ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) ⋮ Premise selection for mathematics by corpus analysis and kernel methods

Uses Software

• Coq
• ML
• Isabelle/HOL
• OTTER
• VAMPIRE
• PVS
• TPTP
• Metis_
• HOL
• E Theorem Prover
• Jahob

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Mathematical induction in Otter-lambda
• Lightweight relevance filtering for machine-generated resolution problems
• Unification under a mixed prefix
• Isabelle/HOL. A proof assistant for higher-order logic
• Automation for interactive proof: first prototype
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• Director strings as combinators
• A new implementation technique for applicative languages
• Another algorithm for bracket abstraction
• Automated Reasoning
• Automated Reasoning
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: Translating higher-order clauses to first-order clauses