Pages that link to "Item:Q2351158"

The following pages link to Extending Sledgehammer with SMT solvers (Q2351158):

Displaying 44 items.

• Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
• Adding decision procedures to SMT solvers using axioms with triggers (Q287384) (← links)
• A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
• A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
• Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
• LEO-II and Satallax on the Sledgehammer test bench (Q1948289) (← links)
• Towards satisfiability modulo parametric bit-vectors (Q2051567) (← links)
• Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
• Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
• Formalizing axiomatic systems for propositional logic in Isabelle/HOL (Q2128791) (← links)
• SMTCoq: a plug-in for integrating SMT solvers into Coq (Q2164216) (← links)
• Relational characterisations of paths (Q2210868) (← links)
• Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support (Q2211865) (← links)
• From LCF to Isabelle/HOL (Q2280211) (← links)
• Automating free logic in HOL, with an experimental application in category theory (Q2303232) (← links)
• Towards bit-width-independent proofs in SMT solvers (Q2305428) (← links)
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry (Q2354917) (← links)
• A decision procedure for (co)datatypes in SMT solvers (Q2360873) (← links)
• From informal to formal proofs in Euclidean geometry (Q2631958) (← links)
• Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
• Second-order properties of undirected graphs (Q2695354) (← links)
• A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Q2817909) (← links)
• Model Finding for Recursive Functions in SMT (Q2817915) (← links)
• Automating Free Logic in Isabelle/HOL (Q2819197) (← links)
• Integrating a SAT solver with an LCF-style theorem prover (Q2848690) (← links)
• Higher-Order Modal Logics: Automation and Applications (Q2970308) (← links)
• Encoding Monomorphic and Polymorphic Types (Q2974796) (← links)
• Mining the Archive of Formal Proofs (Q3453102) (← links)
• LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners (Q3453128) (← links)
• A Decision Procedure for (Co)datatypes in SMT Solvers (Q3454092) (← links)
• Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics (Q3455772) (← links)
• Computer-Supported Exploration of a Categorical Axiomatization of Modeloids (Q5098730) (← links)
• Computer-Supported Analysis of Arguments in Climate Engineering (Q5098745) (← links)
• Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument (Q5126209) (← links)
• A Vernacular for Coherent Logic (Q5495937) (← links)
• (Q5875421) (← links)
• (Q5875431) (← links)
• An automatically verified prototype of the Android permissions system (Q6103592) (← links)
• Dynamic Reconfiguration via Typed Modalities (Q6488473) (← links)
• Propositional proof skeletons (Q6535365) (← links)
• \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format (Q6535368) (← links)
• Dyadic deontic logic in HOL: faithful embedding and meta-theoretical experiments (Q6618558) (← links)
• Solving hard Mizar problems with instantiation and strategy invention (Q6648179) (← links)
• Conditional normative reasoning as a fragment of HOL (Q6650731) (← links)