ETPS
From MaRDI portal
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)
- 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