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

zbMath1002.03002MaRDI QIDQ1847766

Peter B. Andrews

Publication date: 27 October 2002

Published in: Applied Logic Series (Search for Journal in Brave)

zbMATH Keywords

first-order logicpropositional logictype theory

Mathematics Subject Classification ID

Related Items (65)

$n$-fold obstinate and $n$-fold fantastic (pre)filters of $EQ$-algebras ⋮ Integral prefilters and integral EQ-algebras ⋮ The structure of generalized intermediate syllogisms ⋮ Theory morphisms in Church's type theory with quotation and evaluation ⋮ The higher-order prover \textsc{Leo}-II ⋮ Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ A formal theory of intermediate quantifiers ⋮ A comprehensive theory of trichotomous evaluative linguistic expressions ⋮ Proving fairness and implementation correctness of a microkernel scheduler ⋮ Ideal theory on EQ-algebras ⋮ From Classical to Fuzzy Type Theory ⋮ Parametric Church's thesis: synthetic computability without choice ⋮ Logical structure of fuzzy IF-THEN rules ⋮ State theory on bounded hyper EQ-algebras ⋮ Higher-order semantics and extensionality ⋮ Semantics, calculi, and analysis for object-oriented specifications ⋮ GLIVENKO AND KURODA FOR SIMPLE TYPE THEORY ⋮ Syllogisms and 5-square of opposition with intermediate quantifiers in fuzzy natural logic ⋮ TPS: A hybrid automatic-interactive system for developing proofs ⋮ Extensional higher-order paramodulation in Leo-III ⋮ In the Search of a Naive Type Theory ⋮ On good EQ-algebras ⋮ New kinds of hybrid filters of EQ-algebras ⋮ Reasoning about mathematical fuzzy logic and its future ⋮ RECONSTRUCTION OF G. SPENCER BROWN'S THEME ⋮ Non-commutative first-order EQ-logics ⋮ A formal theory of generalized intermediate syllogisms ⋮ Quantified multimodal logics in simple type theory ⋮ Graded Generalized Hexagon in Fuzzy Natural Logic ⋮ What's right with a syntactic approach to theories and models? ⋮ Monotonicity inference for higher-order formulas ⋮ Carnap's early metatheory: scope and limits ⋮ Probabilities on sentences in an expressive logic ⋮ The theory of intermediate quantifiers in fuzzy natural logic revisited and the model of ``many ⋮ On theorem prover-based testing ⋮ Combining and automating classical and non-classical logics in classical higher-order logics ⋮ Graded structures of opposition in fuzzy natural logic ⋮ Carnap's early semantics ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ The seven virtues of simple type theory ⋮ Combined reasoning by automated cooperation ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Elements of model theory in higher-order fuzzy logic ⋮ On fuzzy type theory ⋮ Monotonicity Inference for Higher-Order Formulas ⋮ Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion ⋮ Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners) ⋮ Second-Order Programs with Preconditions ⋮ Higher-order quantifier elimination, counter simulations and fault-tolerant systems ⋮ Extending Sledgehammer with SMT Solvers ⋮ Evaluation of anonymity and confidentiality protocols using theorem proving ⋮ Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics ⋮ ETPS ⋮ Monadic Sequence Testing and Explicit Test-Refinements ⋮ On General Properties of Intermediate Quantifiers ⋮ Combining Theories with Shared Set Operations ⋮ Mechanized metatheory revisited ⋮ An extensible encoding of object-oriented data models in HOL. With an application to IMP++ ⋮ EQ-algebras ⋮ Subtypes in fuzzy type theory ⋮ Model-theoretic conservative extension for definitional theories ⋮ Formal analysis of Peterson's rules for checking validity of syllogisms with intermediate quantifiers ⋮ 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

This page was built for publication: An introduction to mathematical logic and type theory: To truth through proof.