Pages that link to "Item:Q2908482"

The following pages link to Satallax: An Automatic Higher-Order Prover (Q2908482):

Displaying 40 items.

• Satallax (Q18920) (← links)
• MaLeS: a framework for automatic tuning of automated theorem provers (Q286787) (← links)
• The higher-order prover \textsc{Leo}-II (Q287283) (← links)
• Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
• Computer-assisted analysis of the Anderson-Hájek ontological controversy (Q523303) (← links)
• Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
• Improving automation for higher-order proof steps (Q831930) (← links)
• Superposition for full higher-order logic (Q2055874) (← links)
• A Knuth-Bendix-like ordering for orienting combinator equations (Q2096451) (← links)
• A combinator-based superposition calculus for higher-order logic (Q2096452) (← links)
• Lash 1.0 (system description) (Q2104521) (← links)
• Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
• Automating free logic in HOL, with an experimental application in category theory (Q2303232) (← 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)
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
• Cut-elimination for quantified conditional logic (Q2363418) (← links)
• Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
• Internal Guidance for Satallax (Q2817934) (← links)
• Effective Normalization Techniques for HOL (Q2817937) (← links)
• Agent-Based HOL Reasoning (Q2819202) (← links)
• Proofs and Reconstructions (Q2964467) (← links)
• Higher-Order Modal Logics: Automation and Applications (Q2970308) (← links)
• Interacting with Modal Logics in the Coq Proof Assistant (Q3194730) (← links)
• LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners (Q3453128) (← links)
• Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics (Q3455772) (← links)
• A realizability interpretation of Church's simple theory of types (Q4593235) (← links)
• Theorem Proving in Large Formal Mathematics as an Emerging AI Field (Q4913871) (← links)
• (Q4989394) (← links)
• (Q5028439) (← links)
• Practical Proof Search for Coq by Type Inhabitation (Q5048991) (← links)
• The CADE-28 Automated Theorem Proving System Competition – CASC-28 (Q5069650) (← links)
• The CADE-26 automated theorem proving system competition – CASC-26 (Q5145427) (← links)
• Superposition with lambdas (Q5918381) (← links)
• Superposition with lambdas (Q5919500) (← links)
• The 11th IJCAR automated theorem proving system competition – CASC-J11 (Q6095787) (← links)
• Superposition for higher-order logic (Q6156638) (← links)
• Extending a high-performance prover to higher-order logic (Q6536126) (← links)