An introduction to mathematical logic and type theory: To truth through proof.
From MaRDI portal
Publication:1847766
zbMath1002.03002MaRDI QIDQ1847766
Publication date: 27 October 2002
Published in: Applied Logic Series (Search for Journal in Brave)
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Classical first-order logic (03B10) Classical propositional logic (03B05) Computability and recursion theory (03D99)
Related Items
$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
