scientific article; zbMATH DE number 3999882

zbMath0617.03001MaRDI QIDQ4726218

Peter B. Andrews

Publication date: 1986

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

first-order logicpropositional logictype theory

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Classical first-order logic (03B10) Classical propositional logic (03B05)

Related Items (41)

Probabilistic modelling, inference and learning using logical theories ⋮ Combining Model Checking and Deduction ⋮ Rewriting, and equational unification: the higher-order cases ⋮ A semantics for \(\lambda \)Prolog ⋮ HOL Light: An Overview ⋮ Computing verisimilitude ⋮ Probabilistic reasoning in a classical logic ⋮ Using tactics to reformulate formulae for resolution theorem proving ⋮ TPS: A theorem-proving system for classical type theory ⋮ Decidability of fluted logic with identity ⋮ Semantics for abstract clauses ⋮ On connections and higher-order logic ⋮ Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems ⋮ Grammar induction by unification of type-logical lexicons ⋮ Rigid E-unification: NP-completeness and applications to equational matings ⋮ Identity, equality, nameability and completeness. Part II ⋮ Decidability of bounded higher-order unification ⋮ A logical framework combining model and proof theory ⋮ On sets, types, fixed points, and checkerboards ⋮ Data types with errors and exceptions ⋮ Unification under a mixed prefix ⋮ A survey of nonstandard sequent calculi ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ Quantum number theory ⋮ PNL to HOL: from the logic of nominal sets to the logic of higher-order functions ⋮ A partial functions version of Church's simple theory of types ⋮ MBase: Representing knowledge and context for the integration of mathematical software systems ⋮ Abstract deduction and inferential models for type theory ⋮ Completeness in equational hybrid propositional type theory ⋮ General framework of structural similarity between system models ⋮ 2004 Summer Meeting of the Association for Symbolic Logic ⋮ ETPS ⋮ The foundation of a generic theorem prover ⋮ Higher-order unification revisited: Complete sets of transformations ⋮ Universal abstract consistency class and universal refutation ⋮ Higher order unification via explicit substitutions ⋮ Experimenting with Isabelle in ZF set theory ⋮ What holds in a context? ⋮ Combinatory reduction systems: Introduction and survey ⋮ A simple type theory with partial functions and subtypes ⋮ IMPS: An interactive mathematical proof system

This page was built for publication: