ETPS
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Instantiation theory. On the foundations of automated deduction
- scientific article; zbMATH DE number 1082077 (Why is no real title available?)
- scientific article; zbMATH DE number 2003148 (Why is no real title available?)
- A survey of nonstandard sequent calculi
- scientific article; zbMATH DE number 194580 (Why is no real title available?)
- The foundation of a generic theorem prover
- Probabilistic reasoning in a classical logic
- MBase: Representing knowledge and context for the integration of mathematical software systems
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems
- Proving fairness and implementation correctness of a microkernel scheduler
- A partial functions version of Church's simple theory of types
- Exploring properties of normal multimodal logics in simple type theory with \texttt{Leo-II}
- A Proof-theoretic Analysis of Goal-directed Provability
- Theorem proving using equational matings and rigid E -unification
- scientific article; zbMATH DE number 823592 (Why is no real title available?)
- Subtypes in fuzzy type theory
- Abstract deduction and inferential models for type theory
- Using tactics to reformulate formulae for resolution theorem proving
- From classical to fuzzy type theory
- Higher order unification via explicit substitutions
- scientific article; zbMATH DE number 1617310 (Why is no real title available?)
- Non-commutative first-order EQ-logics
- Integral prefilters and integral EQ-algebras
- What's right with a syntactic approach to theories and models?
- Completeness in equational hybrid propositional type theory
- scientific article; zbMATH DE number 1140679 (Why is no real title available?)
- Model generation for natural language interpretation and analysis.
- Rigid E-unification: NP-completeness and applications to equational matings
- Mathematical Knowledge Management
- scientific article; zbMATH DE number 1332654 (Why is no real title available?)
- Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving
- Experimenting with Isabelle in ZF set theory
- A Formal Definition for the Expressive Power of Terminological Knowledge Representation Languages
- A proof-theoretic approach to the static analysis of logic programs
- A finite axiomatization of propositional type theory in pure lambda calculus
- A functional partial semantics for intensional logic
- On Virtues of Many-Valued (Fuzzy) Type Theories
- The seven virtues of simple type theory
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Semantics, calculi, and analysis for object-oriented specifications
- Decidability of bounded higher-order unification
- Graded generalized hexagon in fuzzy natural logic
- Formal analysis of Peterson's rules for checking validity of syllogisms with intermediate quantifiers
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- Carnap's early metatheory: scope and limits
- Mechanized metatheory revisited
- Elements of model theory in higher-order fuzzy logic
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- scientific article; zbMATH DE number 5872266 (Why is no real title available?)
- scientific article; zbMATH DE number 15883 (Why is no real title available?)
- The structure of differential invariants and differential cut elimination
- scientific article; zbMATH DE number 1301860 (Why is no real title available?)
- On general properties of intermediate quantifiers
- scientific article; zbMATH DE number 1863374 (Why is no real title available?)
- Carnap's early semantics
- Higher-order unification revisited: Complete sets of transformations
- A second order theory of data types
- Alonzo church:his life, his work and some of his miracles
- Universal abstract consistency class and universal refutation
- A semantics for \(\lambda \)Prolog
- Rewriting, and equational unification: the higher-order cases
- Frontiers of Combining Systems
- Probabilistic modelling, inference and learning using logical theories
- scientific article; zbMATH DE number 2185659 (Why is no real title available?)
- scientific article; zbMATH DE number 1324444 (Why is no real title available?)
- On theorem prover-based testing
- Engineering and theoretical underpinnings of retrenchment
- Extending Sledgehammer with SMT solvers
- Combinatory reduction systems: Introduction and survey
- scientific article; zbMATH DE number 1911272 (Why is no real title available?)
- HOL Light: An Overview
- TPS: A theorem-proving system for classical type theory
- Monotonicity inference for higher-order formulas
- Theorem Proving in Higher Order Logics
- The structure of generalized intermediate syllogisms
- The higher-order prover \textsc{Leo}-II
- A formal theory of intermediate quantifiers
- A comprehensive theory of trichotomous evaluative linguistic expressions
- A logical framework combining model and proof theory
- Reasoning about mathematical fuzzy logic and its future
- Quantified multimodal logics in simple type theory
- A formal theory of generalized intermediate syllogisms
- On fuzzy type theory
- Syllogisms and 5-square of opposition with intermediate quantifiers in fuzzy natural logic
- Multimodal and intuitionistic logics in simple type theory
- TPS: A hybrid automatic-interactive system for developing proofs
- Combining theories with shared set operations
- Theorem Proving in Higher Order Logics
- EQ-algebra-based fuzzy type theory and its extensions
- HOL-Boogie
- LEO-II
- TPS
- IMP++
- HiLog
- SecureUML
- IMPACT
- HOL-Z
- RAISE
- THF0
This page was built for software: ETPS
