The following pages link to TPS (Q13717):
Displaying 50 items.
- The higher-order prover \textsc{Leo}-II (Q287283) (← links)
- Analytic tableaux for higher-order logic with choice (Q438561) (← links)
- Combining and automating classical and non-classical logics in classical higher-order logics (Q656826) (← links)
- Computer theorem proving in mathematics (Q704001) (← links)
- Mathematical induction in Otter-lambda (Q861715) (← links)
- A proof-centric approach to mathematical assistants (Q865648) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- The seven virtues of simple type theory (Q946569) (← links)
- What holds in a context? (Q1312161) (← links)
- IMPS: An interactive mathematical proof system (Q1319391) (← links)
- Reduction and unification in lambda calculi with a general notion of subtype (Q1340967) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- Comparing approaches to resolution based higher-order theorem proving (Q1868166) (← links)
- Theorem proving with analytic tableaux and related methods. 5th international workshop, TABLEAUX '96, Terrasini, Palermo, Italy, May 15--17, 1996. Proceedings (Q1913544) (← links)
- TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
- Embedding and automating conditional logics in classical higher-order logic (Q1935597) (← links)
- Quantified multimodal logics in simple type theory (Q1945702) (← links)
- LEO-II and Satallax on the Sledgehammer test bench (Q1948289) (← links)
- Lash 1.0 (system description) (Q2104521) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- Limited second-order functionality in a first-order setting (Q2303245) (← links)
- Reducing higher-order theorem proving to a sequence of SAT problems (Q2351156) (← links)
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (Q2655326) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- An intensional type theory: motivation and cut-elimination (Q2732287) (← links)
- EQ-algebra-based fuzzy type theory and its extensions (Q2885176) (← links)
- Rewriting Strategies and Strategic Rewrite Programs (Q2945718) (← links)
- Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations (Q3006121) (← links)
- Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners) (Q3058454) (← links)
- Multimodal and intuitionistic logics in simple type theory (Q3061280) (← links)
- (Q3075241) (← links)
- (Q3086769) (← links)
- (Q3086785) (← links)
- (Q3086786) (← links)
- (Q3086787) (← links)
- Regular Patterns in Second-Order Unification (Q3454122) (← links)
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) (Q3541699) (← links)
- THF0 – The Core of the TPTP Language for Higher-Order Logic (Q3541725) (← links)
- A Nominal Axiomatization of the Lambda Calculus (Q3553919) (← links)
- The CADE-22 automated theorem proving system competition – CASC-22 (Q3561621) (← links)
- Combining Logics in Simple Type Theory (Q3582734) (← links)
- Combining Type Theory and Untyped Set Theory (Q3613410) (← links)
- Supra-logic: using transfinite type theory with type variables for paraconsistency (Q3647220) (← links)
- Terminating Tableaux for the Basic Fragment of Simple Type Theory (Q3648727) (← links)
- (Q4012178) (← links)
- (Q4247078) (← links)
- (Q4264719) (← links)
- Mechanizing coinduction and corecursion in higher-order logic (Q4340418) (← links)
- (Q4428312) (← links)
- (Q4518867) (← links)
