Proof Checking and Logic Programming (Q5743582): Difference between revisions

@@ Property / describes a project that uses @@
+ML
@@ Property / describes a project that uses: ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Twelf
@@ Property / describes a project that uses: Twelf / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+kepler98
@@ Property / describes a project that uses: kepler98 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Abella
@@ Property / describes a project that uses: Abella / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+DRAT-trim
@@ Property / describes a project that uses: DRAT-trim / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+dedukti
@@ Property / describes a project that uses: dedukti / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+seL4
@@ Property / describes a project that uses: seL4 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Teyjus
@@ Property / describes a project that uses: Teyjus / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2400995082
@@ Property / OpenAlex ID: W2400995082 / rank @@
+Normal rank
@@ Property / cites work @@
+Logic Programming with Focusing Proofs in Linear Logic
+Normal rank
@@ Property / cites work @@
+A logical characterization of forward and backward chaining in the inverse method
+Normal rank
@@ Property / cites work @@
+Foundational Proof Certificates in First-Order Logic
+Normal rank
@@ Property / cites work @@
+A formulation of the simple theory of types
@@ Property / cites work: A formulation of the simple theory of types / rank @@
+Normal rank
@@ Property / cites work @@
+Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
+Normal rank
@@ Property / cites work @@
+Q4842975
@@ Property / cites work: Q4842975 / rank @@
+Normal rank
@@ Property / cites work @@
+Call-by-Value  -calculus and LJQ
@@ Property / cites work: Call-by-Value -calculus and LJQ / rank @@
+Normal rank
@@ Property / cites work @@
+A two-level logic approach to reasoning about computations
+Normal rank
@@ Property / cites work @@
+Linear logic
@@ Property / cites work: Linear logic / rank @@
+Normal rank
@@ Property / cites work @@
+A new constructive logic: classic logic
@@ Property / cites work: A new constructive logic: classic logic / rank @@
+Normal rank
@@ Property / cites work @@
+The Four Colour Theorem: Engineering of a Formal Proof
+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 @@
+A proof of the Kepler conjecture
@@ Property / cites work: A proof of the Kepler conjecture / rank @@
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Focusing and polarization in linear, intuitionistic, and classical logics
+Normal rank
@@ Property / cites work @@
+Q5271422
@@ Property / cites work: Q5271422 / rank @@
+Normal rank
@@ Property / cites work @@
+Programming with Higher-Order Logic
@@ Property / cites work: Programming with Higher-Order Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Uniform proofs as a foundation for logic programming
+Normal rank
@@ Property / cites work @@
+DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:5743582