Language peer sets for 2OBJ:
Designed 1995 ↑
1990s languages ↑
Meta-logical framework theorem proveralternate simple view
Country: United Kingdom
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.
2OBJ is built in top of the OBJ system. Logics are defined in 2OBJ by loading a suitable "frame" (a specification of a logics syntax and rules of inference) written in OBJ3. Once a frame is loaded users can then define and apply their own tactics (mechanised proof procedures) to build proofs over user defined theories.
Search in: Google Google scholar World Cat Yahoo Overture DBLP Monash bib NZ IEEE  ACM portal CiteSeer CSB ncstrl jstor Bookfinder