P185
MetiTarski: An Automatic Theorem Prover for Real-Valued Special FunctionsComputational logic: its origins and applications.Natural deduction as higher-order resolutionLEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal IsabelleIntroduction to Milestones in Interactive Theorem ProvingDeciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOLA Formal Proof of Cauchy’s Residue TheoremA modular, efficient formalisation of real algebraic numbersAn Isabelle/HOL Formalisation of Green’s TheoremProofs and ReconstructionsA MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETSApplying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic DecompositionAutomated theorem proving for special functionsMachine Learning for First-Order Theorem ProvingVerifying Hybrid Systems Involving Transcendental FunctionsVerifying multicast-based security protocols using the inductive methodCase Splitting in an Automatic Theorem Prover for Real-Valued Special FunctionsExtending Sledgehammer with SMT SolversLEO-II and Satallax on the Sledgehammer test benchFormal Verification of Cardholder Registration in SETQuantified Multimodal Logics in Simple Type TheoryVerifying multicast-based security protocols using the inductive methodMetiTarski: Past and FutureReal Algebraic Strategies for MetiTarski ProofsExtending Sledgehammer with SMT SolversApplications of MetiTarski in the Verification of Control and Hybrid SystemsFormal verification of analog designs using MetiTarskiLightweight relevance filtering for machine-generated resolution problemsMetiTarski: An Automatic Prover for the Elementary FunctionsThe Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZFTranslating Higher-Order Clauses to First-Order ClausesPrefaceAccountability protocolsAutomation for interactive proof: First prototypeDefining functions on equivalence classesErratum to “Automation for interactive proof: First prototype” [Inform. and Comput. 204 (2006) 1575–1596]Verifying the SET Purchase ProtocolsAn overview of the verification of SETIs the Verification Problem for Cryptographic Protocols Solved?
P50
Q30054495-DB0ECA34-F6B7-43ED-BCD6-78F7D590EDA8Q55174437-08962D84-F226-44D0-8FD5-4F05E70B1B8EQ55894613-931CD0C2-2D21-4984-B16B-15F0BB633F08Q56020733-02E40892-7A25-47DF-A491-897B7854CEE9Q56853390-3fcceb7b-4920-dcbd-8839-0876e15e3a16Q57382527-568604F4-F5D4-476A-8CAB-38E2A730B430Q57382533-2E013E66-CA08-4114-BA3A-04FB9E9CD566Q57382537-9DD3C304-5B80-4445-8EC5-6406B9E8B2E1Q57382539-DF02C255-2FF8-4C80-905B-814DF00F2FF3Q57382542-F8DCE2AE-6BD5-44FA-A154-36EC63DBA60EQ57382545-0CE4A069-11AA-4F18-8ADF-B5AD8E54C403Q57382547-5FC5886F-830A-440A-B5FD-7EB93EAE1CD4Q57382551-DD957CB4-E57E-4C78-92A2-4A2B45C77EF4Q57382553-C272FE7E-DB4A-422F-931A-DBD57292A413Q57382555-2E18583D-CD60-4AA7-818E-6E4B4B344EB2Q57382560-27898B39-4306-425E-B881-F18EC1B78263Q57382565-3394AE3E-CF32-4C8A-A01B-AEF44B91EF46Q57382569-C872026C-6D3B-4E4E-9DE0-5BFCC80FD893Q57382571-AEFAFD89-3F15-461E-8817-D6CF1A142863Q57382576-FB6D559F-77BB-4A9F-9DDA-902E1B99D855Q57382579-3BD99E97-34CD-4055-AAF3-1F69E2D76EAEQ57382584-7BCE2249-7DED-49B3-A949-4F8DF904E067Q57382589-E44CE2B2-22C1-45AF-B302-3761F6D31524Q57382597-28895A7C-61BF-4D67-976A-74BF2D8A15D3Q57382600-CD44556B-A5D3-471F-9D05-41C30786E648Q57382606-94BACCD6-3626-410D-8AAE-A845EFC865AAQ57382616-0827BA15-2370-4A08-AA23-491F6A3D8874Q57382618-CE6A0989-D72E-4022-81E2-BA8FAC0A59D5Q57382620-42F9BD24-5153-48EE-B9DA-3CF5F626CE87Q57382626-DC662126-C36A-4B8E-946B-14DC0869AF90Q57382628-4A88B359-E339-423B-9E5B-EB8B8448FBE1Q57382631-D38B1540-9A5E-46D8-9785-47AE030E1B61Q57382633-DD88D5EC-B874-4A95-8809-C2A25E0540A4Q57382636-AD451E02-9633-4A04-B80F-D9440AD47731Q57382638-40128709-AD07-4428-ABF4-37CA3C77AE04Q57382639-19012A69-6636-4AF4-B480-1E40780EFC94Q57382642-FD001A9F-37D3-4E8F-96A4-DBD4F44A8B28Q57382648-87B831C6-FFAF-47FC-8841-24A227ADD452Q57382652-4A7B170F-D3A6-431D-BBB3-CFA4C873EC5EQ57382655-8E31A51A-DDF7-4F98-A1CC-8FFC79C5A53F
P50
description
American computer scientist
@en
Amerikaans informaticus
@nl
informaticien américain
@fr
name
Lawrence Paulson
@ast
Lawrence Paulson
@ca
Lawrence Paulson
@de
Lawrence Paulson
@en
Lawrence Paulson
@es
Lawrence Paulson
@fr
Lawrence Paulson
@nl
Lawrence Paulson
@sl
لورانس بولسون
@ar
type
label
Lawrence Paulson
@ast
Lawrence Paulson
@ca
Lawrence Paulson
@de
Lawrence Paulson
@en
Lawrence Paulson
@es
Lawrence Paulson
@fr
Lawrence Paulson
@nl
Lawrence Paulson
@sl
لورانس بولسون
@ar
altLabel
Lawrence C. Paulson
@de
Lawrence C. Paulson
@en
Lawrence Charles Paulson
@en
prefLabel
Lawrence Paulson
@ast
Lawrence Paulson
@ca
Lawrence Paulson
@de
Lawrence Paulson
@en
Lawrence Paulson
@es
Lawrence Paulson
@fr
Lawrence Paulson
@nl
Lawrence Paulson
@sl
لورانس بولسون
@ar