The following pages link to Sledgehammer (Q19106):
Displaying 50 items.
- 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)
- Interaction with formal mathematical documents in Isabelle/PIDE (Q2287890) (← links)
- Automating free logic in HOL, with an experimental application in category theory (Q2303232) (← links)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
- Towards bit-width-independent proofs in SMT solvers (Q2305428) (← links)
- Infinite executions of lazy and strict computations (Q2347906) (← links)
- Reducing higher-order theorem proving to a sequence of SAT problems (Q2351156) (← 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)
- On the fine-structure of regular algebra (Q2352506) (← 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)
- Soundness and completeness proofs by coinductive methods (Q2362498) (← links)
- Finding proofs in Tarskian geometry (Q2362499) (← links)
- Automating change of representation for proofs in discrete mathematics (extended version) (Q2364883) (← links)
- Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems (Q2405266) (← links)
- A proof strategy language and proof script generation for Isabelle/HOL (Q2405272) (← 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)
- Internal Guidance for Satallax (Q2817934) (← links)
- Automating Free Logic in Isabelle/HOL (Q2819197) (← links)
- AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic (Q2829278) (← links)
- Mechanizing the Metatheory of Sledgehammer (Q2849493) (← links)
- A Heuristic Prover for Real Inequalities (Q2879243) (← links)
- Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs (Q2891399) (← links)
- Automating Induction with an SMT Solver (Q2891425) (← links)
- Automated and Human Proofs in General Mathematics: An Initial Comparison (Q2891438) (← links)
- Automatic Verification of TLA + Proof Obligations with SMT Solvers (Q2891459) (← links)
- Challenges and Experiences in Managing Large-Scale Proofs (Q2907311) (← links)
- More SPASS with Isabelle (Q2914754) (← links)
- Automated Reasoning in Higher-Order Regular Algebra (Q2915136) (← links)
- Unifying Theories of Programming in Isabelle (Q2948230) (← links)
- Proofs and Reconstructions (Q2964467) (← links)
- Random Forests for Premise Selection (Q2964471) (← links)
- Higher-Order Modal Logics: Automation and Applications (Q2970308) (← links)
- Towards a UTP Semantics for Modelica (Q2971175) (← links)
- An Axiomatic Value Model for Isabelle/UTP (Q2971180) (← links)
- Encoding Monomorphic and Polymorphic Types (Q2974796) (← links)
- Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem (Q3100205) (← links)
- Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL (Q3100212) (← links)
- Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
- Extracting a DPLL Algorithm (Q3178287) (← links)
- Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic (Q3179185) (← links)
- Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm (Q3179390) (← links)
