ETPS

swMATH6302MaRDI QIDQ18433FDOQ18433

Author name not available (Why is that?)

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

Described by source

• An introduction to mathematical logic and type theory: To truth through proof.
• Unnamed Publication

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

• 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?)
• The foundation of a generic theorem prover
• The seven virtues of simple type theory
• A semantics for \(\lambda \)Prolog
• A finite axiomatization of propositional type theory in pure lambda calculus
• Mechanized metatheory revisited
• Title not available (Why is that?)
• The structure of differential invariants and differential cut elimination
• Higher-order unification revisited: Complete sets of transformations
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
• Rewriting, and equational unification: the higher-order cases
• Incorporating quotation and evaluation into Church's type theory
• MBase: Representing knowledge and context for the integration of mathematical software systems
• Incorporating quotation and evaluation into Church's type theory: syntax and semantics
• Universal abstract consistency class and universal refutation
• A proof-theoretic approach to the static analysis of logic programs
• Instantiation theory. On the foundations of automated deduction
• Higher order unification via explicit substitutions
• Elements of model theory in higher-order fuzzy logic
• From classical to fuzzy type theory
• Title not available (Why is that?)
• Theory morphisms in Church's type theory with quotation and evaluation
• Title not available (Why is that?)
• A Proof-theoretic Analysis of Goal-directed Provability
• Title not available (Why is that?)
• Experimenting with Isabelle in ZF set theory
• Probabilistic reasoning in a classical logic
• Semantics, calculi, and analysis for object-oriented specifications
• Title not available (Why is that?)
• Subtypes in fuzzy type theory
• Mathematical Knowledge Management
• Graded generalized hexagon in fuzzy natural logic
• Decidability of bounded higher-order unification
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theorem proving using equational matings and rigid E -unification
• On Virtues of Many-Valued (Fuzzy) Type Theories
• What's right with a syntactic approach to theories and models?
• Model generation for natural language interpretation and analysis.
• Title not available (Why is that?)
• Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formal analysis of Peterson's rules for checking validity of syllogisms with intermediate quantifiers
• Proving fairness and implementation correctness of a microkernel scheduler
• A Formal Definition for the Expressive Power of Terminological Knowledge Representation Languages
• On general properties of intermediate quantifiers
• A survey of nonstandard sequent calculi
• A partial functions version of Church's simple theory of types
• Abstract deduction and inferential models for type theory
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Carnap's early metatheory: scope and limits
• Title not available (Why is that?)
• Using tactics to reformulate formulae for resolution theorem proving
• Rigid E-unification: NP-completeness and applications to equational matings
• Title not available (Why is that?)
• Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving
• 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

This page was built for software: ETPS