swMATH6302MaRDI QIDQ18433FDOQ18433
Author name not available (Why is that?)
Official website: http://gtps.math.cmu.edu/tps-about.html
Cited In (only showing first 100 items - show all)
- A logical framework combining model and proof theory
- Extending Sledgehammer with SMT solvers
- Completeness in equational hybrid propositional type theory
- Reasoning about mathematical fuzzy logic and its future
- Title not available (Why is that?)
- The structure of generalized intermediate syllogisms
- Dependent ML An approach to practical programming with dependent types
- Non-commutative first-order EQ-logics
- A formal theory of generalized intermediate syllogisms
- The higher-order prover \textsc{Leo}-II
- Higher-order semantics and extensionality
- Title not available (Why is that?)
- Monotonicity inference for higher-order formulas
- On fuzzy type theory
- Theorem Proving in Higher Order Logics
- A formal theory of intermediate quantifiers
- A comprehensive theory of trichotomous evaluative linguistic expressions
- Combining and automating classical and non-classical logics in classical higher-order logics
- Combinatory reduction systems: Introduction and survey
- On connections and higher-order logic
- Combined reasoning by automated cooperation
- HOL-Boogie
- LEO-II
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- TPS
- IMP++
- HiLog
- HOL-OCL
- Nuprl
- Oz
- MUSCADET
- Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing
- On theorem prover-based testing
- LFLC 2000
- IMPS
- VSDITLU
- MetaOCaml
- CalcCheck
- Monotonox
- Mcmt
- JPF-SE
- Pesca
- Symbolic automata
- FOOL
- FeatureVis
- HOL-TestGen
- Combining theories with shared set operations
- FALCON
- Leo
- MKRP
- 3TAP
- BLOG
- Hyperproof
- reFLect
- Jordan
- Emacs
- Depth First Search
- Fuzz
- EPGY
- HOL Light QE
- Presburger Automata
- Hotel Key Card
- Robbins Conjecture
- PROVERB
- Cambridge LCF
- CoqInE
- AGES
- Theorem Proving in Higher Order Logics
- TPS: A theorem-proving system for classical type theory
- Quantified multimodal logics in simple type theory
- Logical structure of fuzzy IF-THEN rules
- Adimen-SUMO
- On good EQ-algebras
- Carnap's early semantics
- Syllogisms and 5-square of opposition with intermediate quantifiers in fuzzy natural logic
- TPS: A hybrid automatic-interactive system for developing proofs
- Alonzo church:his life, his work and some of his miracles
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- Analysis of generalized square of opposition with intermediate quantifiers
- Extending Sledgehammer with SMT solvers
- A Nominal Axiomatization of the Lambda Calculus
- EQ-algebra-based fuzzy type theory and its extensions
- EQ-algebras
- IMPS: An interactive mathematical proof system
- Partial and nested recursive function definitions in higher-order logic
- Engineering and theoretical underpinnings of retrenchment
- Multimodal and intuitionistic logics in simple type theory
- A simple type theory with partial functions and subtypes
- HOL Light: An Overview
- Integral prefilters and integral EQ-algebras
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- A second order theory of data types
- Frontiers of Combining Systems
- 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}
- A functional partial semantics for intensional logic
- Probabilistic modelling, inference and learning using logical theories
- Title not available (Why is that?)
This page was built for software: ETPS
