Towards Logical Frameworks in the Heterogeneous Tool Set Hets

DOI10.1007/978-3-642-28412-0_10zbMath1278.68286OpenAlexW111349018WikidataQ57389377 ScholiaQ57389377MaRDI QIDQ2890328

Florian Rabe, Till Mossakowski, Kristina Sojakova, Mihai Codescu, Fulya Horozal, Michael Kohlhase

Publication date: 8 June 2012

Published in: Recent Trends in Algebraic Development Techniques (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-28412-0_10

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Abstract data types; algebraic specification (68Q65) Combinatory logic and lambda calculus (03B40)

Related Items

A Proof Theoretic Interpretation of Model Theoretic Hiding, A scalable module system, The Distributed Ontology, Modeling and Specification Language – DOL, A logical framework combining model and proof theory, Structure-preserving diagram operators, Parchments for CafeOBJ Logics, A Maude environment for CafeOBJ, Project Abstract: Logic Atlas and Integrator (LATIN)

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• CASL
• Mizar
• Maude
• Nuprl
• Twelf
• Hets
• Delphin

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Representing model theory in a type-theoretical logical framework
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Structured theory presentations and logic representations
• Isabelle. A generic theorem prover
• Encoding modal logics in logical frameworks
• Isabelle/HOL. A proof assistant for higher-order logic
• CASL: the Common Algebraic Specification Language.
• Structural cut elimination. I: Intuitionistic and classical logic
• Development graphs -- proof management for structured specifications
• Institution-independent model theory
• Formalising foundations of mathematics
• A framework for defining logics
• Institutions: abstract model theory for specification and programming
• An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
• A logical framework combining model and proof theory
• A formulation of the simple theory of types