An Interactive Driver for Goal-directed Proof Strategies (Q5166499): Difference between revisions

@@ Property / describes a project that uses @@
+APT
@@ Property / describes a project that uses: APT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+VAMPIRE
@@ Property / describes a project that uses: VAMPIRE / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Oz Explorer
@@ Property / describes a project that uses: Oz Explorer / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.entcs.2008.12.099
+Normal rank
@@ Property / OpenAlex ID @@
+W2146583274
@@ Property / OpenAlex ID: W2146583274 / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Crafting a Proof Assistant
@@ Property / cites work: Crafting a Proof Assistant / rank @@
+Normal rank
@@ Property / cites work @@
+User interaction with the Matita proof assistant
@@ Property / cites work: User interaction with the Matita proof assistant / rank @@
+Normal rank
@@ Property / cites work @@
+Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
+Normal rank
@@ Property / cites work @@
+A two-level approach towards lean proof-checking
@@ Property / cites work: A two-level approach towards lean proof-checking / rank @@
+Normal rank
@@ Property / cites work @@
+The calculus of constructions
@@ Property / cites work: The calculus of constructions / rank @@
+Normal rank
@@ Property / cites work @@
+Automation for interactive proof: first prototype
@@ Property / cites work: Automation for interactive proof: first prototype / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Reasoning
@@ Property / cites work: Automated Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Linear resolution with selection function
@@ Property / cites work: Linear resolution with selection function / rank @@
+Normal rank
@@ Property / cites work @@
+Q3992908
@@ Property / cites work: Q3992908 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3150300
@@ Property / cites work: Q3150300 / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+Working with Mathematical Structures in Type Theory
+Normal rank