2OBJ is a ”meta-logical framework theorem prover”, i.e., a system that can be tailored to prove theorems in any desired logical system, and can also prove theorems about proofs in that system.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Meseguer, José: Twenty years of rewriting logic (2012)
- Martí-Oliet, Narciso; Palomino, Miguel; Verdejo, Alberto: Strategies and simulations in a semantic framework (2007)
- Nicolás, Joaquín; Toval, Ambrosio; Arenas, Aurelio; Alcalde, Juan: Formal validation and verification of atomic resolution microscope control and topography (2001)
- Sampaio, Augusto: An algebraic approach to compiler design (1997)
- Martí-Oliet, Narciso; Meseguer, José: Rewriting logic as a logical and semantic framework (1996)
- Reetz, Ralf; Kropf, Thomas: A flowgraph semantics of VHDL: Toward a VHDL verification workbench in HOL. (1995)
- Goguen, Joseph A.; Diaconescu, Răzvan: Towards an algebraic semantics for the object paradigm (1994)
- Goguen, Joseph; Diaconescu, Răzvan: An Oxford survey of order sorted algebra (1994)
- Stavridou, Victoria: Gordon’s computer: A hardware verification case study in OBJ3 (1994)