ETPS
From MaRDI portal
Software:18433
No author found.
Related Items (only showing first 100 items - show all)
$n$-fold obstinate and $n$-fold fantastic (pre)filters of $EQ$-algebras ⋮ Unnamed Item ⋮ Rewriting, and equational unification: the higher-order cases ⋮ From Classical to Fuzzy Type Theory ⋮ A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification ⋮ Unnamed Item ⋮ Dependent ML An approach to practical programming with dependent types ⋮ A Proof-theoretic Analysis of Goal-directed Provability ⋮ Higher-order semantics and extensionality ⋮ Unnamed Item ⋮ Modal Sequent Calculi Labelled with Truth Values: Completeness, Duality and Analyticity ⋮ Unnamed Item ⋮ Theorem proving using equational matings and rigid E -unification ⋮ RECONSTRUCTION OF G. SPENCER BROWN'S THEME ⋮ Graded Generalized Hexagon in Fuzzy Natural Logic ⋮ A Formal Definition for the Expressive Power of Terminological Knowledge Representation Languages ⋮ A Hoare Logic for Call-by-Value Functional Programs ⋮ Identity, equality, nameability and completeness. Part II ⋮ Unnamed Item ⋮ Fluted formulas and the limits of decidability ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ The Structure of Differential Invariants and Differential Cut Elimination ⋮ A Nominal Axiomatization of the Lambda Calculus ⋮ A logical framework combining model and proof theory ⋮ Automated Termination Analysis for Programs with Second-Order Recursion ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On sets, types, fixed points, and checkerboards ⋮ Unnamed Item ⋮ Frontiers of Combining Systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Alonzo church:his life, his work and some of his miracles ⋮ Unnamed Item ⋮ Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing ⋮ A Theory of System Interaction: Components, Interfaces, and Services ⋮ Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Mathematical Fuzzy Logic in Modeling of Natural Language Semantics ⋮ A partial functions version of Church's simple theory of types ⋮ MBase: Representing knowledge and context for the integration of mathematical software systems ⋮ Unnamed Item ⋮ Extending Sledgehammer with SMT Solvers ⋮ Evaluation of anonymity and confidentiality protocols using theorem proving ⋮ Unnamed Item ⋮ Recent Trends in Algebraic Development Techniques ⋮ Unnamed Item ⋮ Theorem Proving in Higher Order Logics ⋮ Theorem Proving in Higher Order Logics ⋮ On General Properties of Intermediate Quantifiers ⋮ Supra-logic: using transfinite type theory with type variables for paraconsistency ⋮ Combining Theories with Shared Set Operations ⋮ Algebraic Methodology and Software Technology ⋮ Unnamed Item ⋮ Mathematical Knowledge Management ⋮ Unnamed Item ⋮ Integral prefilters and integral EQ-algebras ⋮ EQ-algebra-based fuzzy type theory and its extensions ⋮ The structure of generalized intermediate syllogisms ⋮ Theory morphisms in Church's type theory with quotation and evaluation ⋮ The higher-order prover \textsc{Leo}-II ⋮ A formal theory of intermediate quantifiers ⋮ A comprehensive theory of trichotomous evaluative linguistic expressions ⋮ Proving fairness and implementation correctness of a microkernel scheduler ⋮ A second order theory of data types ⋮ Probabilistic modelling, inference and learning using logical theories ⋮ Combining Model Checking and Deduction ⋮ A Bit of History Related to Logic Based on Equality ⋮ A semantics for \(\lambda \)Prolog ⋮ HOL Light: An Overview ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Parametric Church's thesis: synthetic computability without choice ⋮ Logical structure of fuzzy IF-THEN rules ⋮ Unnamed Item ⋮ Computing verisimilitude ⋮ Probabilistic reasoning in a classical logic ⋮ 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 ⋮ Theorem proving with analytic tableaux and related methods. 5th international workshop, TABLEAUX '96, Terrasini, Palermo, Italy, May 15--17, 1996. Proceedings ⋮ Unnamed Item ⋮ Using tactics to reformulate formulae for resolution theorem proving ⋮ TPS: A theorem-proving system for classical type theory ⋮ Decidability of fluted logic with identity ⋮ On good EQ-algebras ⋮ Reasoning about mathematical fuzzy logic and its future ⋮ Non-commutative first-order EQ-logics ⋮ A formal theory of generalized intermediate syllogisms ⋮ Quantified multimodal logics in simple type theory ⋮ What's right with a syntactic approach to theories and models? ⋮ On connections and higher-order logic ⋮ Monotonicity inference for higher-order formulas ⋮ Carnap's early metatheory: scope and limits ⋮ 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
This page was built for software: ETPS
