ETPS
From MaRDI portal
Cited in
(only showing first 100 items - show all)- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- EQ-algebras
- A second order theory of data types
- Instantiation theory. On the foundations of automated deduction
- Universal abstract consistency class and universal refutation
- Experimenting with Isabelle in ZF set theory
- Combinatory reduction systems: Introduction and survey
- A simple type theory with partial functions and subtypes
- HOL-Boogie
- IMPS: An interactive mathematical proof system
- LEO-II
- A semantics for Prolog
- TPS
- Using tactics to reformulate formulae for resolution theorem proving
- IMP++
- HiLog
- SecureUML
- IMPACT
- HOL-Z
- RAISE
- THF0
- Non-commutative first-order EQ-logics
- Carnap's early metatheory: scope and limits
- Incorporating quotation and evaluation into Church's type theory
- Quantum number theory
- HOL-OCL
- The foundation of a generic theorem prover
- Higher-order unification revisited: Complete sets of transformations
- Higher order unification via explicit substitutions
- Nuprl
- Oz
- MUSCADET
- Computing verisimilitude
- 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
- Decidability of fluted logic with identity
- Quantified multimodal logics in simple type theory
- Grammar induction by unification of type-logical lexicons
- LFLC 2000
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- Experiences from exporting major proof assistant libraries
- VSDITLU
- Formal analysis of Peterson's rules for checking validity of syllogisms with intermediate quantifiers
- IMPS
- MetaOCaml
- Integral prefilters and integral EQ-algebras
- Parametric Church's thesis: synthetic computability without choice
- CalcCheck
- The theory of intermediate quantifiers in fuzzy natural logic revisited and the model of ``many
- Graded structures of opposition in fuzzy natural logic
- Monotonox
- A survey of nonstandard sequent calculi
- Completeness in equational hybrid propositional type theory
- Mechanized metatheory revisited
- Subtypes in fuzzy type theory
- Model-theoretic conservative extension for definitional theories
- Analysis of generalized square of opposition with intermediate quantifiers
- Extending Sledgehammer with SMT solvers
- EQ-algebras from the point of view of generalized algebras with fuzzy equalities
- Theory morphisms in Church's type theory with quotation and evaluation
- Mcmt
- Probabilistic reasoning in a classical logic
- Semantics, calculi, and analysis for object-oriented specifications
- JPF-SE
- Probabilities on sentences in an expressive logic
- Decidability of bounded higher-order unification
- Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book
- Model generation for natural language interpretation and analysis.
- Symbolic automata
- Pesca
- FOOL
- scientific article; zbMATH DE number 1617290 (Why is no real title available?)
- scientific article; zbMATH DE number 1617295 (Why is no real title available?)
- scientific article; zbMATH DE number 1617310 (Why is no real title available?)
- scientific article; zbMATH DE number 1614693 (Why is no real title available?)
- FeatureVis
- The structure of generalized intermediate syllogisms
- Incorporating quotation and evaluation into Church's type theory: syntax and semantics
- Monadic Sequence Testing and Explicit Test-Refinements
- The higher-order prover \textsc{Leo}-II
- EQ-algebra-based fuzzy type theory and its extensions
- Glivenko and Kuroda for simple type theory
- HOL-TestGen
- Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations
- scientific article; zbMATH DE number 2185659 (Why is no real title available?)
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Second-order programs with preconditions
- Multimodal and intuitionistic logics in simple type theory
- A finite axiomatization of propositional type theory in pure lambda calculus
- 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}
- A proof-theoretic approach to the static analysis of logic programs
- The teaching tool CalcCheck: a proof-checker for Gries and Schneider's ``Logical approach to discrete math
- MKRP
- Leo
- On Virtues of Many-Valued (Fuzzy) Type Theories
- Combining Model Checking and Deduction
- HOL Light: An Overview
- FALCON
- 3TAP
This page was built for software: ETPS
