H ? « ‹ ← → › »

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

2OBJ(ID:3684/obj006)

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.

Structures:
Related languages
OBJ2 → 2OBJ   Extension of
OBJ3 → 2OBJ   Written using

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