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)

• 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
• A formal theory of intermediate quantifiers
• A comprehensive theory of trichotomous evaluative linguistic expressions
• Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners)
• Combining and automating classical and non-classical logics in classical higher-order logics
• Combinatory reduction systems: Introduction and survey
• Higher order unification via explicit substitutions
• On connections and higher-order logic
• Elements of model theory in higher-order fuzzy logic
• Combined reasoning by automated cooperation
• Title not available (Why is that?)
• Probabilistic reasoning in a classical logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing
• On theorem prover-based testing
• Extending Sledgehammer with SMT Solvers
• Subtypes in fuzzy type theory
• Theorem Proving in Higher Order Logics
• TPS: A theorem-proving system for classical type theory
• Quantified multimodal logics in simple type theory
• Logical structure of fuzzy IF-THEN rules
• Theorem proving using equational matings and rigid E -unification
• On Virtues of Many-Valued (Fuzzy) Type Theories
• On good EQ-algebras
• Carnap's early semantics
• Model generation for natural language interpretation and analysis.
• Syllogisms and 5-square of opposition with intermediate quantifiers in fuzzy natural logic
• TPS: A hybrid automatic-interactive system for developing proofs
• Title not available (Why is that?)
• Alonzo church:his life, his work and some of his miracles
• An extensible encoding of object-oriented data models in HOL. With an application to IMP++
• Analysis of generalized square of opposition with intermediate quantifiers
• Extending Sledgehammer with SMT solvers
• A Nominal Axiomatization of the Lambda Calculus
• From Classical to Fuzzy Type Theory
• EQ-algebra-based fuzzy type theory and its extensions
• EQ-algebras
• IMPS: An interactive mathematical proof system
• Title not available (Why is that?)
• Title not available (Why is that?)
• The Structure of Differential Invariants and Differential Cut Elimination
• Partial and nested recursive function definitions in higher-order logic
• Engineering and theoretical underpinnings of retrenchment
• Proving fairness and implementation correctness of a microkernel scheduler
• A Formal Definition for the Expressive Power of Terminological Knowledge Representation Languages
• Title not available (Why is that?)
• Abstract deduction and inferential models for type theory
• Multimodal and intuitionistic logics in simple type theory
• A simple type theory with partial functions and subtypes
• HOL Light: An Overview
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Title not available (Why is that?)
• Rigid E-unification: NP-completeness and applications to equational matings
• Combining Theories with Shared Set Operations
• Title not available (Why is that?)
• Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving
• 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?)

This page was built for software: ETPS