H ? « »

Language peer sets for 2OBJ:
United Kingdom
United Kingdom/1995
Designed 1995
1990s languages
Fifth generation
Post-Cold War


Meta-logical framework theorem prover 

alternate simple view
Country: United Kingdom
Designed 1995

Oxford U

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.

Related languages
OBJ2 2OBJ   Extension of
OBJ3 2OBJ   Written using

Search in: Google  Google scholar  World Cat  Yahoo  Overture  DBLP  Monash bib  NZ  IEEE  ACM portal  CiteSeer  CSB  ncstrl  jstor  Bookfinder