Analogical type theory
The paper aims at a formalization of analogy reasoning. An analogical intuitionistic type theory (AITT) is proposed. AITT is developed from Martin-Löf's intuitionistic type theory MITT and from the analogical calculus \(LK_A\) [the authors, Theor. Comput. Sci. 113, 211-230 (1993; Zbl 0784.68083)]. Martin-Löf's intuitionistic type theory is presented in section 2. In section 3, fundamentals of the AITT-analogy theory are given. Analogy between types is defined as follows. Let \(A\) and \(B\) be types (sets). Further, let us consider mappings \(f\) and \(g\), such that \(f : A \to B\), \(g : B \to A\), the equivalence relations \(\sim_f\), \(\sim_g\), and mappings \([f] : A/ \sim_f \to B/ \sim_g\), \([g] : B/ \sim_g \to A/ \sim_f\).
- Intuitive minimal abduction in sequent calculi
- Analogy calculus
- Analogy and axiomatics
- scientific article; zbMATH DE number 4057475 (Why is no real title available?)
- scientific article; zbMATH DE number 1302060 (Why is no real title available?)
- scientific article; zbMATH DE number 1302061 (Why is no real title available?)
- Dialectica models of type theory
This page was built for publication: Analogical type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1895393)
