The following pages link to ETPS (Q18433):
Displayed 50 items.
- TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
- Decidability of fluted logic with identity (Q1924331) (← links)
- Quantified multimodal logics in simple type theory (Q1945702) (← links)
- Grammar induction by unification of type-logical lexicons (Q1959226) (← links)
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems (Q2031422) (← links)
- Experiences from exporting major proof assistant libraries (Q2069875) (← links)
- Formal analysis of Peterson's rules for checking validity of syllogisms with intermediate quantifiers (Q2092450) (← links)
- Integral prefilters and integral EQ-algebras (Q2122478) (← links)
- Parametric Church's thesis: synthetic computability without choice (Q2151397) (← links)
- The theory of intermediate quantifiers in fuzzy natural logic revisited and the model of ``many'' (Q2219168) (← links)
- Graded structures of opposition in fuzzy natural logic (Q2228352) (← links)
- A survey of nonstandard sequent calculi (Q2259014) (← links)
- Completeness in equational hybrid propositional type theory (Q2278838) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Subtypes in fuzzy type theory (Q2328911) (← links)
- Model-theoretic conservative extension for definitional theories (Q2333319) (← links)
- Analysis of generalized square of opposition with intermediate quantifiers (Q2350484) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- EQ-algebras from the point of view of generalized algebras with fuzzy equalities (Q2351584) (← links)
- Theory morphisms in Church's type theory with quotation and evaluation (Q2364672) (← links)
- Probabilistic reasoning in a classical logic (Q2390656) (← links)
- Semantics, calculi, and analysis for object-oriented specifications (Q2390933) (← links)
- Probabilities on sentences in an expressive logic (Q2446673) (← links)
- Decidability of bounded higher-order unification (Q2456577) (← links)
- Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book (Q2462639) (← links)
- Model generation for natural language interpretation and analysis. (Q2492154) (← links)
- (Q2722014) (← links)
- (Q2722020) (← links)
- (Q2722041) (← links)
- (Q2723416) (← links)
- Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics (Q2817296) (← links)
- Monadic Sequence Testing and Explicit Test-Refinements (Q2827440) (← links)
- EQ-algebra-based fuzzy type theory and its extensions (Q2885176) (← links)
- GLIVENKO AND KURODA FOR SIMPLE TYPE THEORY (Q2921007) (← links)
- Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations (Q3006121) (← links)
- (Q3024833) (← links)
- Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners) (Q3058454) (← links)
- Second-Order Programs with Preconditions (Q3058455) (← links)
- Multimodal and intuitionistic logics in simple type theory (Q3061280) (← links)
- (Q3086781) (← links)
- (Q3086786) (← links)
- (Q3086787) (← links)
- (Q3086788) (← links)
- The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider’s “Logical Approach to Discrete Math” (Q3100213) (← links)
- On Virtues of Many-Valued (Fuzzy) Type Theories (Q3145134) (← links)
- Combining Model Checking and Deduction (Q3176378) (← links)
- HOL Light: An Overview (Q3183517) (← links)
- General framework of structural similarity between system models (Q3356149) (← links)
- 2004 Summer Meeting of the Association for Symbolic Logic (Q3370624) (← links)
- A Bit of History Related to Logic Based on Equality (Q3454805) (← links)