TPS: A hybrid automatic-interactive system for developing proofs (Q865629): Difference between revisions

@@ Property / describes a project that uses @@
+PVS
@@ Property / describes a project that uses: PVS / rank @@
+Normal rank
@@ 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 @@
+IMPS
@@ Property / describes a project that uses: IMPS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOT
@@ Property / describes a project that uses: HOT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Leo
@@ Property / describes a project that uses: Leo / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Lambda-Clam
@@ Property / describes a project that uses: Lambda-Clam / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ETPS
@@ Property / describes a project that uses: ETPS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nuprl
@@ Property / describes a project that uses: Nuprl / 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.jal.2005.10.002
+Normal rank
@@ Property / OpenAlex ID @@
+W1987549075
@@ Property / OpenAlex ID: W1987549075 / rank @@
+Normal rank
@@ Property / cites work @@
+TPS: A theorem-proving system for classical type theory
+Normal rank
@@ Property / cites work @@
+Q2723416
@@ Property / cites work: Q2723416 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3338232
@@ Property / cites work: Q3338232 / rank @@
+Normal rank
@@ Property / cites work @@
+A compact representation of proofs
@@ Property / cites work: A compact representation of proofs / rank @@
+Normal rank
@@ Property / cites work @@
+On connections and higher-order logic
@@ Property / cites work: On connections and higher-order logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809075
@@ Property / cites work: Q4809075 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751367
@@ Property / cites work: Q2751367 / rank @@
+Normal rank
@@ Property / cites work @@
+An introduction to mathematical logic and type theory: To truth through proof.
+Normal rank
@@ Property / cites work @@
+SET-VAR
@@ Property / cites work: SET-VAR / rank @@
+Normal rank
@@ Property / cites work @@
+Resolution in type theory
@@ Property / cites work: Resolution in type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Higher-order semantics and extensionality
@@ Property / cites work: Higher-order semantics and extensionality / rank @@
+Normal rank
@@ Property / cites work @@
+A unification algorithm for typed \(\bar\lambda\)-calculus
+Normal rank
@@ Property / cites work @@
+Dissolution
@@ Property / cites work: Dissolution / rank @@
+Normal rank
@@ Property / cites work @@
+Gazing: An approach to the problem of definition and lemma use
+Normal rank
@@ Property / cites work @@
+A man-machine theorem-proving system
@@ Property / cites work: A man-machine theorem-proving system / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving via General Matings
@@ Property / cites work: Theorem Proving via General Matings / rank @@
+Normal rank
@@ Property / cites work @@
+Q4692618
@@ Property / cites work: Q4692618 / rank @@
+Normal rank
@@ Property / cites work @@
+Eliminating dublication with the hyper-linking strategy
+Normal rank
@@ Property / cites work @@
+Graph-Based Algorithms for Boolean Function Manipulation
+Normal rank
@@ Property / cites work @@
+Q4247078
@@ Property / cites work: Q4247078 / rank @@
+Normal rank
@@ Property / cites work @@
+Model generation for natural language interpretation and analysis.
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+The foundation of a generic theorem prover
@@ Property / cites work: The foundation of a generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle. A generic theorem prover
@@ Property / cites work: Isabelle. A generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+IMPS: An interactive mathematical proof system
@@ Property / cites work: IMPS: An interactive mathematical proof system / rank @@
+Normal rank
@@ Property / cites work @@
+Q2767046
@@ Property / cites work: Q2767046 / rank @@
+Normal rank
@@ Property / cites work @@
+A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
+Normal rank
@@ Property / cites work @@
+Structural Analysis of Narratives with the Coq Proof Assistant
+Normal rank
@@ Property / cites work @@
+Q4790648
@@ Property / cites work: Q4790648 / rank @@
+Normal rank
@@ Property / cites work @@
+Unifying Theories in ProofPower-Z
@@ Property / cites work: Unifying Theories in ProofPower-Z / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809051
@@ Property / cites work: Q4809051 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated deduction - CADE-15. 15th international conference, Lindau, Germany, July 5--10, 1998. Proceedings
+Normal rank
@@ Property / cites work @@
+Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7--10, 1999. Proceedings
+Normal rank
@@ Property / cites work @@
+Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27--30, 2002. Proceedings
+Normal rank