ETPS

swMATH6302MaRDI QIDQ18433FDOQ18433

Author name not available (Why is that?)

Described by source

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

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