ETPS
From MaRDI portal
Software:18433
swMATH6302MaRDI QIDQ18433FDOQ18433
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- The theory of intermediate quantifiers in fuzzy natural logic revisited and the model of ``many
- Integral prefilters and integral EQ-algebras
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- Decidability of fluted logic with identity
- A second order theory of data types
- Frontiers of Combining Systems
- Identity, equality, nameability and completeness. Part II
- Title not available (Why is that?)
- Model-theoretic conservative extension for definitional theories
- Title not available (Why is that?)
- Graded structures of opposition in fuzzy natural logic
- Mechanized metatheory revisited
- Title not available (Why is that?)
- Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics
- 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
- Universal abstract consistency class and universal refutation
- EQ-algebras from the point of view of generalized algebras with fuzzy equalities
- Instantiation theory. On the foundations of automated deduction
- Computing verisimilitude
- Theorem proving with analytic tableaux and related methods. 5th international workshop, TABLEAUX '96, Terrasini, Palermo, Italy, May 15--17, 1996. Proceedings
- Theory morphisms in Church's type theory with quotation and evaluation
- Title not available (Why is that?)
- Quantum number theory
- A Proof-theoretic Analysis of Goal-directed Provability
- Title not available (Why is that?)
- Experimenting with Isabelle in ZF set theory
- Parametric Church's thesis: synthetic computability without choice
- Semantics, calculi, and analysis for object-oriented specifications
- On General Properties of Intermediate Quantifiers
- Title not available (Why is that?)
- Mathematical Knowledge Management
- Fluted formulas and the limits of decidability
- Decidability of bounded higher-order unification
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- What's right with a syntactic approach to theories and models?
- A Theory of System Interaction: Components, Interfaces, and Services
- Title not available (Why is that?)
- Experiences from exporting major proof assistant libraries
- Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems
- Formal analysis of Peterson's rules for checking validity of syllogisms with intermediate quantifiers
- Grammar induction by unification of type-logical lexicons
- A survey of nonstandard sequent calculi
- A partial functions version of Church's simple theory of types
- Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations
- Carnap's early metatheory: scope and limits
- Using tactics to reformulate formulae for resolution theorem proving
- A Hoare Logic for Call-by-Value Functional Programs
- Title not available (Why is that?)
- Second-Order Programs with Preconditions
- $n$-fold obstinate and $n$-fold fantastic (pre)filters of $EQ$-algebras
- Evaluation of anonymity and confidentiality protocols using theorem proving
- A Bit of History Related to Logic Based on Equality
- Probabilities on sentences in an expressive logic
- Title not available (Why is that?)
- Algebraic Methodology and Software Technology
- Supra-logic: using transfinite type theory with type variables for paraconsistency
- Automated Termination Analysis for Programs with Second-Order Recursion
- Modal Sequent Calculi Labelled with Truth Values: Completeness, Duality and Analyticity
- Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book
- Glivenko and Kuroda for simple type theory
- RECONSTRUCTION OF G. SPENCER BROWN'S THEME
- Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion
- Title not available (Why is that?)
- The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider’s “Logical Approach to Discrete Math”
- General framework of structural similarity between system models
- Monadic Sequence Testing and Explicit Test-Refinements
- 2004 Summer Meeting of the Association for Symbolic Logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Mathematical Fuzzy Logic in Modeling of Natural Language Semantics
- Combining Model Checking and Deduction
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- On sets, types, fixed points, and checkerboards
- Recent Trends in Algebraic Development Techniques
- A logical framework combining model and proof theory
- A functional partial semantics for intensional logic
- Completeness in equational hybrid propositional type theory
- Probabilistic modelling, inference and learning using logical theories
- The foundation of a generic theorem prover
- Reasoning about mathematical fuzzy logic and its future
- Title not available (Why is that?)
- The seven virtues of simple type theory
- Graded Generalized Hexagon in Fuzzy Natural Logic
- A semantics for \(\lambda \)Prolog
- The structure of generalized intermediate syllogisms
- Dependent ML An approach to practical programming with dependent types
- Higher-order unification revisited: Complete sets of transformations
- Non-commutative first-order EQ-logics
- A formal theory of generalized intermediate syllogisms
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- 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
This page was built for software: ETPS