Programming and verifying a declarative first-order prover in Isabelle/HOL (Q5145439): Difference between revisions

@@ Property / describes a project that uses @@
+Isabelle/jEdit
@@ Property / describes a project that uses: Isabelle/jEdit / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+GitHub
@@ Property / describes a project that uses: GitHub / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Completeness theorem
@@ Property / describes a project that uses: Completeness theorem / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Superposition Calculus
@@ Property / describes a project that uses: Superposition Calculus / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Sledgehammer
@@ Property / describes a project that uses: Sledgehammer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Metamath
@@ Property / describes a project that uses: Metamath / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+FOL Fitting
@@ Property / describes a project that uses: FOL Fitting / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Verified Prover
@@ Property / describes a project that uses: Verified Prover / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Extending Sledgehammer with SMT Solvers
@@ Property / cites work: Extending Sledgehammer with SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Soundness and completeness proofs by coinductive methods
+Normal rank
@@ Property / cites work @@
+Visual Theorem Proving with the Incredible Proof Machine
+Normal rank
@@ Property / cites work @@
+Q3235339
@@ Property / cites work: Q3235339 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof assistants: history, ideas and future
@@ Property / cites work: Proof assistants: history, ideas and future / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+Code Generation via Higher-Order Rewrite Systems
@@ Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751354
@@ Property / cites work: Q2751354 / rank @@
+Normal rank
@@ Property / cites work @@
+Towards Self-verification of HOL Light
@@ Property / cites work: Towards Self-verification of HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Q3618853
@@ Property / cites work: Q3618853 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4619818
@@ Property / cites work: Q4619818 / rank @@
+Normal rank
@@ Property / cites work @@
+Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
+Normal rank
@@ Property / cites work @@
+How to Write a Proof
@@ Property / cites work: How to Write a Proof / rank @@
+Normal rank
@@ Property / cites work @@
+How to write a 21\(^{\text{st}}\) century proof
@@ Property / cites work: How to write a 21\(^{\text{st}}\) century proof / rank @@
+Normal rank
@@ Property / cites work @@
+Q2753598
@@ Property / cites work: Q2753598 / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Q4124795
@@ Property / cites work: Q4124795 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
+Normal rank
@@ Property / cites work @@
+Seventy-five problems for testing automatic theorem provers
+Normal rank
@@ Property / cites work @@
+Formalization of the Resolution Calculus for First-Order Logic
+Normal rank
@@ Property / cites work @@
+The Gödel Completeness Theorem for Uncountable Languages
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.3233/aic-180764
+Normal rank
@@ Property / OpenAlex ID @@
+W2797950816
@@ Property / OpenAlex ID: W2797950816 / rank @@
+Normal rank