The following pages link to Lawrence Charles Paulson (Q352969):
Displaying 50 items.
- (Q242598) (redirect page) (← links)
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772) (← links)
- The higher-order prover \textsc{Leo}-II (Q287283) (← links)
- Case splitting in an automatic theorem prover for real-valued special functions (Q352970) (← links)
- (Q800738) (redirect page) (← links)
- A higher-order implementation of rewriting (Q800739) (← links)
- Verifying the SET purchase protocols (Q861698) (← links)
- MetiTarski: An automatic theorem prover for real-valued special functions (Q972422) (← links)
- Lightweight relevance filtering for machine-generated resolution problems (Q1006731) (← links)
- Verifying the unification algorithm in LCF (Q1060023) (← links)
- Constructing recursion operators in intuitionistic type theory (Q1094421) (← links)
- Proving termination of normalization functions for conditional expressions (Q1101251) (← links)
- Set theory for verification. I: From foundations to functions (Q1319386) (← links)
- Isabelle. A generic theorem prover (Q1331625) (← links)
- Isabelle/HOL. A proof assistant for higher-order logic (Q1600086) (← links)
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (Q1725844) (← links)
- Organizing numerical theories using axiomatic type classes (Q1774558) (← links)
- The foundation of a generic theorem prover (Q1823013) (← links)
- Set theory for verification. II: Induction and recursion (Q1904402) (← links)
- Quantified multimodal logics in simple type theory (Q1945702) (← links)
- LEO-II and Satallax on the Sledgehammer test bench (Q1948289) (← links)
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L (Q1961914) (← links)
- Using machine learning to improve cylindrical algebraic decomposition (Q2009221) (← links)
- Bayesian ranking for strategy scheduling in automated theorem provers (Q2104545) (← links)
- A modular first formalisation of combinatorial design theory (Q2128787) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL (Q2303242) (← links)
- An Isabelle/HOL formalisation of Green's theorem (Q2323451) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- Machine learning for first-order theorem proving (Q2351414) (← links)
- Automation for interactive proof: first prototype (Q2432769) (← links)
- Translating higher-order clauses to first-order clauses (Q2471742) (← links)
- Mechanizing compositional reasoning for concurrent systems: some lessons (Q2576572) (← links)
- A simple formalization and proof for the mutilated chess board (Q2720299) (← links)
- Automated theorem proving for special functions (Q2819703) (← links)
- An Isabelle/HOL Formalisation of Green’s Theorem (Q2829238) (← links)
- A Formal Proof of Cauchy’s Residue Theorem (Q2829261) (← links)
- MetiTarski’s Menagerie of Cooperating Systems (Q2849476) (← links)
- Real Algebraic Strategies for MetiTarski Proofs (Q2907335) (← links)
- MetiTarski: Past and Future (Q2914728) (← links)
- A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS (Q2940885) (← links)
- Proofs and Reconstructions (Q2964467) (← links)
- Multimodal and intuitionistic logics in simple type theory (Q3061280) (← links)
- (Q3086787) (← links)
- (Q3330551) (← links)
- A Formalisation of Finite Automata Using Hereditarily Finite Sets (Q3454094) (← links)
- Extending a Resolution Prover for Inequalities on Elementary Functions (Q3498456) (← links)
- The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF (Q3507465) (← links)
- Source-Level Proof Reconstruction for Interactive Theorem Proving (Q3523178) (← links)
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) (Q3541699) (← links)
