Pages that link to "Item:Q2471742"

The following pages link to Translating higher-order clauses to first-order clauses (Q2471742):

Displaying 37 items.

• Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
• Learning-assisted theorem proving with millions of lemmas (Q485842) (← links)
• Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
• Making PVS accessible to generic services by interpretation in a universal format (Q1687752) (← links)
• HOL(y)Hammer: online ATP service for HOL Light (Q2018657) (← links)
• A Knuth-Bendix-like ordering for orienting combinator equations (Q2096451) (← links)
• A combinator-based superposition calculus for higher-order logic (Q2096452) (← links)
• Relational characterisations of paths (Q2210868) (← links)
• Limited second-order functionality in a first-order setting (Q2303245) (← links)
• Extending SMT solvers to higher-order logic (Q2305406) (← links)
• Restricted combinatory unification (Q2305407) (← links)
• GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) (Q2305414) (← links)
• Extending Sledgehammer with SMT solvers (Q2351158) (← links)
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
• Premise selection for mathematics by corpus analysis and kernel methods (Q2352489) (← links)
• Automating change of representation for proofs in discrete mathematics (extended version) (Q2364883) (← links)
• From informal to formal proofs in Euclidean geometry (Q2631958) (← links)
• Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
• Semantic subtyping with an SMT solver (Q2913944) (← links)
• Encoding Monomorphic and Polymorphic Types (Q2974796) (← links)
• MaLeCoP Machine Learning Connection Prover (Q3010374) (← links)
• Validating QBF Validity in HOL4 (Q3088005) (← links)
• Proving Valid Quantified Boolean Formulas in HOL Light (Q3088006) (← links)
• Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
• Expressing Polymorphic Types in a Many-Sorted Language (Q3172884) (← links)
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance (Q3541722) (← links)
• (Q4989394) (← links)
• Extending Sledgehammer with SMT Solvers (Q5200019) (← links)
• Sort It Out with Monotonicity (Q5200026) (← links)
• A Foundational View on Integration Problems (Q5200111) (← links)
• Mining State-Based Models from Proof Corpora (Q5495930) (← links)
• Sledgehammer: Judgement Day (Q5747754) (← links)
• A FORMAL SYSTEM FOR EUCLID’S<i>ELEMENTS</i> (Q5850985) (← links)
• Superposition with lambdas (Q5918381) (← links)
• Superposition with lambdas (Q5919500) (← links)
• (Q6079227) (← links)