TPS

swMATH973MaRDI QIDQ13717FDOQ13717

Author name not available (Why is that?)

Official website: http://gtps.math.cmu.edu/tps-about.html

Described by source

• TPS: A hybrid automatic-interactive system for developing proofs
• Unnamed Publication

Cited In (only showing first 100 items - show all)

• A realizability interpretation of Church's simple theory of types
• Lash 1.0 (system description)
• Supra-logic: using transfinite type theory with type variables for paraconsistency
• Extensional higher-order paramodulation in Leo-III
• Functions-as-constructors higher-order unification: extended pattern unification
• Reducing higher-order theorem proving to a sequence of SAT problems
• Superposition with lambdas
• Theorem proving with analytic tableaux and related methods. 5th international workshop, TABLEAUX '96, Terrasini, Palermo, Italy, May 15--17, 1996. Proceedings
• Limited second-order functionality in a first-order setting
• Title not available (Why is that?)
• Decidable higher-order unification problems
• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• Combining logics in simple type theory
• On sets, types, fixed points, and checkerboards
• Some historical reflections
• Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations
• Automated Deduction – CADE-20
• Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
• Exploring properties of normal multimodal logics in simple type theory with \texttt{Leo-II}
• Mechanizing coinduction and corecursion in higher-order logic
• Superposition with lambdas
• Embedding and automating conditional logics in classical higher-order logic
• Building reliable, high-performance networks with the Nuprl proof development system
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The seven virtues of simple type theory
• Rewriting strategies and strategic rewrite programs
• Mathematical Knowledge Management
• Title not available (Why is that?)
• KI 2004: Advances in Artificial Intelligence
• Title not available (Why is that?)
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• Mechanizing Mathematical Reasoning
• 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
• The higher-order prover \textsc{Leo}-II
• An intensional type theory: Motivation and cut-elimination
• MBase: Representing knowledge and context for the integration of mathematical software systems
• Title not available (Why is that?)
• Analytic tableaux for higher-order logic with choice
• Theorem Proving in Higher Order Logics
• Mathematical induction in Otter-lambda
• A proof-centric approach to mathematical assistants
• Title not available (Why is that?)
• Combining and automating classical and non-classical logics in classical higher-order logics
• Computer theorem proving in mathematics
• Regular patterns in second-order unification
• Computer supported mathematics with \(\Omega\)MEGA
• Reducing higher-order theorem proving to a sequence of SAT problems
• Combining Type Theory and Untyped Set Theory
• Strategic computation and deduction
• What holds in a context?
• LEO-II
• IsaWin
• Isabelle/ZF
• TAS
• TeXmacs
• ETPS
• I-SATCHMO
• Nuprl
• Satallax
• Title not available (Why is that?)
• MathXpert
• MBase
• IMPS
• VSDITLU
• PhoX
• MathWeb
• Specware
• HOT
• Terminating tableaux for the basic fragment of simple type theory
• The CADE-22 automated theorem proving system competition -- CASC-22
• OMEGA
• Leo-III
• InKa
• Leo
• Lambda-Clam
• Omega-ANTS
• Waldmeister
• Bliksem
• KOMET
• PROTEIN
• SKIL
• Emacs
• PROVERB
• Analytic tableaux for higher-order logic with choice
• Comparing approaches to resolution based higher-order theorem proving
• Theorem Proving in Higher Order Logics
• TPS: A theorem-proving system for classical type theory
• Quantified multimodal logics in simple type theory
• Adimen-SUMO
• Reduction and unification in lambda calculi with a general notion of subtype
• A Nominal Axiomatization of the Lambda Calculus
• Title not available (Why is that?)
• EQ-algebra-based fuzzy type theory and its extensions
• IMPS: An interactive mathematical proof system
• A partial functions version of Church's simple theory of types

This page was built for software: TPS