TPS
From MaRDI portal
Cited in
(only showing first 100 items - show all)- What holds in a context?
- IMPS: An interactive mathematical proof system
- LEO-II
- Reduction and unification in lambda calculi with a general notion of subtype
- Proof-search in type-theoretic languages: An introduction
- THF0
- PVS
- IsaWin
- TAS
- Isabelle/ZF
- TeXmacs
- ETPS
- Comparing approaches to resolution based higher-order theorem proving
- I-SATCHMO
- Nuprl
- Satallax
- Theorem proving with analytic tableaux and related methods. 5th international workshop, TABLEAUX '96, Terrasini, Palermo, Italy, May 15--17, 1996. Proceedings
- TPS: A theorem-proving system for classical type theory
- Embedding and automating conditional logics in classical higher-order logic
- Quantified multimodal logics in simple type theory
- LEO-II and Satallax on the Sledgehammer test bench
- MathXpert
- MBase
- VSDITLU
- Lash 1.0 (system description)
- IMPS
- Functions-as-constructors higher-order unification: extended pattern unification
- PhoX
- MathWeb
- Limited second-order functionality in a first-order setting
- Reducing higher-order theorem proving to a sequence of SAT problems
- Specware
- HOT
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Extensional higher-order paramodulation in Leo-III
- An intensional type theory: Motivation and cut-elimination
- The higher-order prover \textsc{Leo}-II
- EQ-algebra-based fuzzy type theory and its extensions
- Rewriting strategies and strategic rewrite programs
- Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations
- Leo-III
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Multimodal and intuitionistic logics in simple type theory
- scientific article; zbMATH DE number 5850137 (Why is no real title available?)
- Some historical reflections
- Strategic computation and deduction
- scientific article; zbMATH DE number 5872266 (Why is no real title available?)
- Exploring properties of normal multimodal logics in simple type theory with \texttt{Leo-II}
- Waldmeister
- Leo
- InKa
- Lambda-Clam
- OMEGA
- Omega-ANTS
- PROTEIN
- Bliksem
- KOMET
- Regular patterns in second-order unification
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- A Nominal Axiomatization of the Lambda Calculus
- The CADE-22 automated theorem proving system competition -- CASC-22
- Combining logics in simple type theory
- Combining Type Theory and Untyped Set Theory
- Supra-logic: using transfinite type theory with type variables for paraconsistency
- Terminating tableaux for the basic fragment of simple type theory
- SKIL
- Emacs
- scientific article; zbMATH DE number 67454 (Why is no real title available?)
- PROVERB
- scientific article; zbMATH DE number 1301855 (Why is no real title available?)
- scientific article; zbMATH DE number 1348466 (Why is no real title available?)
- Mechanizing coinduction and corecursion in higher-order logic
- Analytic tableaux for higher-order logic with choice
- scientific article; zbMATH DE number 1980938 (Why is no real title available?)
- scientific article; zbMATH DE number 1538012 (Why is no real title available?)
- scientific article; zbMATH DE number 1543304 (Why is no real title available?)
- A realizability interpretation of Church's simple theory of types
- On sets, types, fixed points, and checkerboards
- scientific article; zbMATH DE number 2154400 (Why is no real title available?)
- scientific article; zbMATH DE number 1863374 (Why is no real title available?)
- scientific article; zbMATH DE number 2090316 (Why is no real title available?)
- Building reliable, high-performance networks with the Nuprl proof development system
- The CADE-28 Automated Theorem Proving System Competition – CASC-28
- Adimen-SUMO
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Reducing higher-order theorem proving to a sequence of SAT problems
- Decidable higher-order unification problems
- Automated Deduction – CADE-20
- KI 2004: Advances in Artificial Intelligence
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Mechanizing Mathematical Reasoning
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- Analytic tableaux for higher-order logic with choice
- A partial functions version of Church's simple theory of types
- Mathematical Knowledge Management
- Superposition with lambdas
- Superposition with lambdas
- MBase: Representing knowledge and context for the integration of mathematical software systems
This page was built for software: TPS
