/////////////////////////////////////////////////
// DO NOT EDIT THIS SOURCE CODE FILE DIRECTLY. //
// IT IS AUTOGENERATED BY npm run build-db. //
/////////////////////////////////////////////////
// Instead, edit database/footer.js, database/generate.js, or any of the
// .putdown or .smackdown files recursively stored in any subfolder of the
// database folder.
// This file begins with the database as a large JSON object,
// then ends with JavaScript code that provides access to it.
const testingDatabase = [
{
"filename": "/matching tests/test 1.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P Q)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(and P Q) (and a (or b c))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP a\n\t\tQ (or b c)\n\t)\n)\n"
},
{
"filename": "/matching tests/test 10.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P x)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P x) (A 1 2 3)\n\t(@apply P x) (A 2 1 3)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 11.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P x y)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P x) (f 1 2)\n\t(@apply P y) (f 1 2)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tx f\n\t\ty f\n\t\tP (@lambda v , (v 1 2))\n\t)\n\t( // solution 2\n\t\tx 1\n\t\ty 1\n\t\tP (@lambda v , (f v 2))\n\t)\n\t( // solution 3\n\t\tx 2\n\t\ty 2\n\t\tP (@lambda v , (f 1 v))\n\t)\n\t( // solution 4\n\t\tx (f 1 2)\n\t\ty (f 1 2)\n\t\tP (@lambda v , v)\n\t)\n\t( // solution 5\n\t\tP (@lambda v , (f 1 2))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 12.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P x)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P x) (g k (e 2))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tx (g k (e 2))\n\t\tP (@lambda v , v)\n\t)\n\t( // solution 2\n\t\tx g\n\t\tP (@lambda v , (v k (e 2)))\n\t)\n\t( // solution 3\n\t\tx k\n\t\tP (@lambda v , (g v (e 2)))\n\t)\n\t( // solution 4\n\t\tx (e 2)\n\t\tP (@lambda v , (g k v))\n\t)\n\t( // solution 5\n\t\tx e\n\t\tP (@lambda v , (g k (v 2)))\n\t)\n\t( // solution 6\n\t\tx 2\n\t\tP (@lambda v , (g k (e v)))\n\t)\n\t( // solution 7\n\t\tP (@lambda v , (g k (e 2)))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 13.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P x)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P x) (f a a)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tx (f a a)\n\t\tP (@lambda v , v)\n\t)\n\t( // solution 2\n\t\tx f\n\t\tP (@lambda v , (v a a))\n\t)\n\t( // solution 3\n\t\tx a\n\t\tP (@lambda v , (f a v))\n\t)\n\t( // solution 4\n\t\tx a\n\t\tP (@lambda v , (f v a))\n\t)\n\t( // solution 5\n\t\tx a\n\t\tP (@lambda v , (f v v))\n\t)\n\t( // solution 6\n\t\tP (@lambda v , (f a a))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 14.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P x)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P x) (f a a)\n\tx b\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tx b\n\t\tP (@lambda v , (f a a))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 15.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P x)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P x) (f a a)\n\tx f\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tx f\n\t\tP (@lambda v , (v a a))\n\t)\n\t( // solution 2\n\t\tx f\n\t\tP (@lambda v , (f a a))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 16.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P a Q b)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P a) (eq 3 3)\n\t(@apply Q b) (gt 5 4)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\ta (eq 3 3)\n\t\tP (@lambda v , v)\n\t\tb (gt 5 4)\n\t\tQ (@lambda v , v)\n\t)\n\t( // solution 2\n\t\ta eq\n\t\tP (@lambda v , (v 3 3))\n\t\tb (gt 5 4)\n\t\tQ (@lambda v , v)\n\t)\n\t( // solution 3\n\t\ta 3\n\t\tP (@lambda v , (eq v v))\n\t\tb (gt 5 4)\n\t\tQ (@lambda v , v)\n\t)\n\t( // solution 4\n\t\ta 3\n\t\tP (@lambda v , (eq v 3))\n\t\tb (gt 5 4)\n\t\tQ (@lambda v , v)\n\t)\n\t( // solution 5\n\t\ta 3\n\t\tP (@lambda v , (eq 3 v))\n\t\tb (gt 5 4)\n\t\tQ (@lambda v , v)\n\t)\n\t( // solution 6\n\t\tP (@lambda v , (eq 3 3))\n\t\tb (gt 5 4)\n\t\tQ (@lambda v , v)\n\t)\n\t( // solution 7\n\t\ta (eq 3 3)\n\t\tP (@lambda v , v)\n\t\tb gt\n\t\tQ (@lambda v , (v 5 4))\n\t)\n\t( // solution 8\n\t\ta eq\n\t\tP (@lambda v , (v 3 3))\n\t\tb gt\n\t\tQ (@lambda v , (v 5 4))\n\t)\n\t( // solution 9\n\t\ta 3\n\t\tP (@lambda v , (eq v v))\n\t\tb gt\n\t\tQ (@lambda v , (v 5 4))\n\t)\n\t( // solution 10\n\t\ta 3\n\t\tP (@lambda v , (eq v 3))\n\t\tb gt\n\t\tQ (@lambda v , (v 5 4))\n\t)\n\t( // solution 11\n\t\ta 3\n\t\tP (@lambda v , (eq 3 v))\n\t\tb gt\n\t\tQ (@lambda v , (v 5 4))\n\t)\n\t( // solution 12\n\t\tP (@lambda v , (eq 3 3))\n\t\tb gt\n\t\tQ (@lambda v , (v 5 4))\n\t)\n\t( // solution 13\n\t\ta (eq 3 3)\n\t\tP (@lambda v , v)\n\t\tb 5\n\t\tQ (@lambda v , (gt v 4))\n\t)\n\t( // solution 14\n\t\ta eq\n\t\tP (@lambda v , (v 3 3))\n\t\tb 5\n\t\tQ (@lambda v , (gt v 4))\n\t)\n\t( // solution 15\n\t\ta 3\n\t\tP (@lambda v , (eq v v))\n\t\tb 5\n\t\tQ (@lambda v , (gt v 4))\n\t)\n\t( // solution 16\n\t\ta 3\n\t\tP (@lambda v , (eq v 3))\n\t\tb 5\n\t\tQ (@lambda v , (gt v 4))\n\t)\n\t( // solution 17\n\t\ta 3\n\t\tP (@lambda v , (eq 3 v))\n\t\tb 5\n\t\tQ (@lambda v , (gt v 4))\n\t)\n\t( // solution 18\n\t\tP (@lambda v , (eq 3 3))\n\t\tb 5\n\t\tQ (@lambda v , (gt v 4))\n\t)\n\t( // solution 19\n\t\ta (eq 3 3)\n\t\tP (@lambda v , v)\n\t\tb 4\n\t\tQ (@lambda v , (gt 5 v))\n\t)\n\t( // solution 20\n\t\ta eq\n\t\tP (@lambda v , (v 3 3))\n\t\tb 4\n\t\tQ (@lambda v , (gt 5 v))\n\t)\n\t( // solution 21\n\t\ta 3\n\t\tP (@lambda v , (eq v v))\n\t\tb 4\n\t\tQ (@lambda v , (gt 5 v))\n\t)\n\t( // solution 22\n\t\ta 3\n\t\tP (@lambda v , (eq v 3))\n\t\tb 4\n\t\tQ (@lambda v , (gt 5 v))\n\t)\n\t( // solution 23\n\t\ta 3\n\t\tP (@lambda v , (eq 3 v))\n\t\tb 4\n\t\tQ (@lambda v , (gt 5 v))\n\t)\n\t( // solution 24\n\t\tP (@lambda v , (eq 3 3))\n\t\tb 4\n\t\tQ (@lambda v , (gt 5 v))\n\t)\n\t( // solution 25\n\t\ta (eq 3 3)\n\t\tP (@lambda v , v)\n\t\tQ (@lambda v , (gt 5 4))\n\t)\n\t( // solution 26\n\t\ta eq\n\t\tP (@lambda v , (v 3 3))\n\t\tQ (@lambda v , (gt 5 4))\n\t)\n\t( // solution 27\n\t\ta 3\n\t\tP (@lambda v , (eq v v))\n\t\tQ (@lambda v , (gt 5 4))\n\t)\n\t( // solution 28\n\t\ta 3\n\t\tP (@lambda v , (eq v 3))\n\t\tQ (@lambda v , (gt 5 4))\n\t)\n\t( // solution 29\n\t\ta 3\n\t\tP (@lambda v , (eq 3 v))\n\t\tQ (@lambda v , (gt 5 4))\n\t)\n\t( // solution 30\n\t\tP (@lambda v , (eq 3 3))\n\t\tQ (@lambda v , (gt 5 4))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 17.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables a b P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(eq a b) (eq t 1)\n\t(@apply P a) (gt t 0)\n\t(@apply P b) (gt 1 0)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\ta t\n\t\tb 1\n\t\tP (@lambda v , (gt v 0))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 18.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables a b P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(eq a b) (eq t 1)\n\t(@apply P a) (gt 1 0)\n\t(@apply P b) (gt t 0)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 19.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables a b P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(eq a b) (eq t 1)\n\t(@apply P a) (eq (plus t 1) 2)\n\t(@apply P b) (eq (plus 1 1) 2)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\ta t\n\t\tb 1\n\t\tP (@lambda v , (eq (plus v 1) 2))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 2.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables X Y)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(multiply (plus X Y) (minus X Y)) (multiply (plus 3 k) (minus 3 p))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 20.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables a b P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(eq a b) (eq t 1)\n\t(@apply P a) (eq (plus 1 1) 2)\n\t(@apply P b) (eq (plus t 1) 2)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 21.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables a b P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(eq a b) (eq 1 2)\n\t(@apply P a) (eq (plus 1 1) 2)\n\t(@apply P b) (eq (plus 2 2) 2)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\ta 1\n\t\tb 2\n\t\tP (@lambda v , (eq (plus v v) 2))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 22.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables a b P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(eq a b) (eq 1 2)\n\t(@apply P a) (eq (plus 1 1) 2)\n\t(@apply P b) (eq (plus 2 1) 2)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\ta 1\n\t\tb 2\n\t\tP (@lambda v , (eq (plus v 1) 2))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 23.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables a b P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(eq a b) (eq 1 2)\n\t(@apply P a) (eq (plus 1 1) 2)\n\t(@apply P b) (eq (plus 1 2) 2)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\ta 1\n\t\tb 2\n\t\tP (@lambda v , (eq (plus 1 v) 2))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 24.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables a b P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(eq a b) (eq 1 2)\n\t(@apply P a) (eq (plus 1 1) 2)\n\t(@apply P b) (eq (plus 1 1) 2)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\ta 1\n\t\tb 2\n\t\tP (@lambda v , (eq (plus 1 1) 2))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 25.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables a b P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(eq a b) (eq 1 2)\n\t(@apply P a) (eq (plus 1 1) 2)\n\t(@apply P b) (eq (plus 2 2) 1)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 26.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables a b P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(eq a b) (eq 1 2)\n\t(@apply P a) (eq (plus 1 1) 2)\n\t(@apply P b) (eq (plus 1 1) 1)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 27.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables a b P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(eq a b) (eq x y)\n\t(@apply P a) (exists y , (neq y x))\n\t(@apply P b) (exists y , (neq y y))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 28.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(forall x , (@apply P x)) (forall x , (gte x 0))\n\t(@apply P t) (gte 7 0)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tt 7\n\t\tP (@lambda v , (gte v 0))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 29.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(forall x , (@apply P x)) (forall x , (gte x 0))\n\t(@apply P t) (gte 7 7)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 3.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(and (@apply P 1) (@apply P 2)) (and (neq 0 1) (neq 0 2))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (neq 0 v))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 30.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(forall x , (@apply P x)) (forall x , Q)\n\t(@apply P t) Q\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , Q)\n\t)\n)\n"
},
{
"filename": "/matching tests/test 31.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(forall x , (@apply P x)) (forall s , (eq (sq s) s))\n\t(@apply P t) (eq (sq 1) 1)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (eq (sq v) v))\n\t\tt 1\n\t)\n)\n"
},
{
"filename": "/matching tests/test 32.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(forall x , (@apply P x)) (forall x , (R x y))\n\t(@apply P t) (R x 3)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 33.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(forall x , (@apply P x)) (forall x , (R x y))\n\t(@apply P t) (R 3 y)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (R v y))\n\t\tt 3\n\t)\n)\n"
},
{
"filename": "/matching tests/test 34.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(forall x , (@apply P x)) (forall x , (R x x))\n\t(@apply P t) (R 3 3)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (R v v))\n\t\tt 3\n\t)\n)\n"
},
{
"filename": "/matching tests/test 35.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(forall x , (@apply P x)) (forall x , (R x x))\n\t(@apply P t) (R 3 x)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 36.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(forall x , (@apply P x)) (forall x , (R x x))\n\t(@apply P t) (R x 3)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 37.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(forall x , (@apply P x)) (forall x , (R x x))\n\t(@apply P t) (R x x)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (R v v))\n\t\tt x\n\t)\n)\n"
},
{
"filename": "/matching tests/test 38.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(forall x , (@apply P x)) (forall s , (eq (plus s s) r))\n\t(@apply P t) (eq (plus t s) r)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 39.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(forall x , (@apply P x)) (forall x , (eq x x))\n\t(@apply P t) (eq (iff P Q) (iff P Q))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (eq v v))\n\t\tt (iff P Q)\n\t)\n)\n"
},
{
"filename": "/matching tests/test 4.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P T)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(forall x , (@apply P x)) (forall r , (gt (plus (sq r) 1) 0))\n\t(@apply P T) (gt (plus (sq -9) 1) 0)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tT -9\n\t\tP (@lambda v , (gt (plus (sq v) 1) 0))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 40.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof a , (r a a))\n\t(forall x , (@apply P x)) (forall b , (r b b))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t(\n\t\tP (@lambda v , (r v v))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 41.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof a , (r a a))\n\t(forall x , (@apply P x)) (forall b , (r b b))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (r v v))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 42.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof a , (r a a))\n\t(forall y , (@apply P y)) (forall b , (r b b))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (r v v))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 43.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof a , (r a a))\n\t(forall y , (@apply P y)) (forall b , (r b b))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (r v v))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 44.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof a , (gt a 3))\n\t(forall y , (@apply P y)) (forall a , (gt a 3))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (gt v 3))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 45.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof a , (gt a 3))\n\t(forall y , (@apply P y)) (forall x , (gt x 3))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (gt v 3))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 46.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof T , (R T T))\n\t(forall y , (@apply P y)) (forall T , (R T T))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (R v v))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 47.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof T , (R T T))\n\t(forall y , (@apply P y)) (forall x , (R T x))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 48.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof y , (neq 0 1))\n\t(forall y , (@apply P y)) (forall z , (neq 0 1))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (neq 0 1))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 49.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof b , (eq (minus b b) 0))\n\t(forall y , (@apply P y)) (forall c , (eq (minus b c) 0))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 5.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables X P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(w (w X (@apply P X)) (forall x , (@apply P x)))\n\t(w (w k (lt (plus k 1) 5)) (forall s , (lt (plus s 1) 5)))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tX k\n\t\tP (@lambda v , (lt (plus v 1) 5))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 50.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof a , (gt a 3))\n\t(forall x , (@apply P x)) (forall a , (gt a 3))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (gt v 3))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 51.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof a , (gt a 3))\n\t(forall x , (@apply P x)) (forall x , (gt x 3))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t(\n\t\tP (@lambda v , (gt v 3))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 52.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof T , (R T T))\n\t(forall x , (@apply P x)) (forall T , (R T T))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (R v v))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 53.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof T , (R T T))\n\t(forall x , (@apply P x)) (forall x , (R T x))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 54.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof y , (neq 0 1))\n\t(forall x , (@apply P x)) (forall y , (neq 0 1))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (neq 0 1))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 55.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof x , (eq x x))\n\t(forall y , (@apply P y)) (forall x , (eq x x))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (eq v v))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 56.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(Subproof x , (@apply P x)) (Subproof x , (exists y , (lt x y)))\n\t(forall x , (@apply P x)) (forall y , (exists y , (lt y y)))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 57.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P t) (gt 1 0)\n\t(exists x , (@apply P x)) (exists x , (gt x 0))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (gt v 0))\n\t\tt 1\n\t)\n)\n"
},
{
"filename": "/matching tests/test 58.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P t) (eq (choose 6 3) 20)\n\t(exists x , (@apply P x)) (exists n , (eq (choose 6 n) 20))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (eq (choose 6 v) 20))\n\t\tt 3\n\t)\n)\n"
},
{
"filename": "/matching tests/test 59.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P t) (lt (pow t x) 5)\n\t(exists x , (@apply P x)) (exists x , (lt (pow x x) 5))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 6.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P Q)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(w (exists x , (@apply P x)) (forall y , (implies (@apply P y) Q)) Q) (w (exists x , (eq (cubed x) -1)) (forall x , (implies (eq (cubed x) -1) (lt x 5))) (lt x 5))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 60.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P t) (neq x t)\n\t(exists x , (@apply P x)) (exists y , (neq y t))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (neq v t))\n\t\tt x\n\t)\n)\n"
},
{
"filename": "/matching tests/test 61.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P t) (neq x t)\n\t(exists x , (@apply P x)) (exists x , (neq x x))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 62.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P t)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P t) (forall t , (eq t t))\n\t(exists x , (@apply P x)) (exists x , (forall t , (eq x t)))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 63.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P 0) (gte 0 0)\n\t(forall k , (implies (@apply P k) (@apply P (plus k 1)))) (forall n , (implies (gte n 0) (gte (plus n 1) 0)))\n\t(forall n , (@apply P n)) (forall n , (gte n 0))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (gte v 0))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 64.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P 0) (eq (plus 0 0) 0)\n\t(forall k , (implies (@apply P k) (@apply P (plus k 1)))) (forall m , (implies (eq (plus m 0) m) (eq (plus (plus m 1) 0) (plus m 1))))\n\t(forall n , (@apply P n)) (forall k , (eq (plus k 0) k))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (eq (plus v 0) v))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 65.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P 0) (P 0)\n\t(forall k , (implies (@apply P k) (@apply P (plus k 1)))) (forall k , (implies (P k) (P (plus k 1))))\n\t(forall n , (@apply P n)) (forall n , (P n))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (P v))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 66.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P 0) (eq 7 5)\n\t(forall k , (implies (@apply P k) (@apply P (plus k 1)))) (forall n , (implies (eq 7 5) (eq 7 5)))\n\t(forall n , (@apply P n)) (forall n , (eq 7 5))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (eq 7 5))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 67.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P 0) (R n 1)\n\t(forall k , (implies (@apply P k) (@apply P (plus k 1)))) (forall m , (implies (R m 1) (R (plus m 1) 1)))\n\t(forall n , (@apply P n)) (forall m , (R m 1))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 68.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P 0) (gte k 0)\n\t(forall k , (implies (@apply P k) (@apply P (plus k 1)))) (forall k , (implies (gte k k) (gte k (plus k 1))))\n\t(forall n , (@apply P n)) (forall n , (gte n k))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 69.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P 0) (gte n 0)\n\t(forall k , (implies (@apply P k) (@apply P (plus k 1)))) (forall k , (implies (gte n k) (gte n (plus k 1))))\n\t(forall n , (@apply P n)) (forall n , (gte n n))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 7.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P x y)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P x) (b 2)\n\t(@apply P y) (b 3)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tx (b 2)\n\t\ty (b 3)\n\t\tP (@lambda v , v)\n\t)\n\t( // solution 2\n\t\tx 2\n\t\ty 3\n\t\tP (@lambda v , (b v))\n\t)\n)\n"
},
{
"filename": "/matching tests/test 70.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P 0) (gte 0 0)\n\t(forall k , (implies (@apply P k) (@apply P (plus k 1)))) (forall n , (implies (gte n 0) (gte 0 (plus n 1))))\n\t(forall n , (@apply P n)) (forall n , (gte 0 0))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 71.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P Q)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(exists x , (@apply P x)) (exists x , (eq (sq x) 1))\n\t(forall x , (implies (@apply P x) Q)) (forall x , (implies (eq (sq x) 1) (gte 1 0)))\n\tQ (gte 1 0)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (eq (sq v) 1))\n\t\tQ (gte 1 0)\n\t)\n)\n"
},
{
"filename": "/matching tests/test 72.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P Q)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(exists x , (@apply P x)) (exists x , (eq (sq x) 1))\n\t(forall x , (implies (@apply P x) Q)) (forall x , (implies (eq (sq x) 1) (lte x 1)))\n\tQ (lte x 1)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 73.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P Q)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(exists x , (@apply P x)) (exists x , (gt x 0))\n\t(forall x , (implies (@apply P x) Q)) (implies (forall x , (gt x 0)) (gt -1 0))\n\tQ (gt -1 0)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 74.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P Q)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(exists x , (@apply P x)) (exists x , (gt x 0))\n\t(forall x , (implies (@apply P x) Q)) (forall x , (implies (gt x 0) (gt -1 0)))\n\tQ (gt -1 0)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (gt v 0))\n\t\tQ (gt -1 0)\n\t)\n)\n"
},
{
"filename": "/matching tests/test 75.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P Q)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(exists x , (@apply P x)) (exists m , (gt m 0))\n\t(forall x , (implies (@apply P x) Q)) (forall m , (implies (gt m 0) (gt -1 0)))\n\tQ (gt -1 0)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (gt v 0))\n\t\tQ (gt -1 0)\n\t)\n)\n"
},
{
"filename": "/matching tests/test 76.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P Q)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(exists x , (@apply P x)) (exists x , (gt x 0))\n\t(forall y , (implies (@apply P y) Q)) (forall x , (implies (gt x 0) (gt -1 0)))\n\tQ (gt -1 0)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (gt v 0))\n\t\tQ (gt -1 0)\n\t)\n)\n"
},
{
"filename": "/matching tests/test 77.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P Q)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(exists x , (@apply P x)) (exists m , (gt m 0))\n\t(forall y , (implies (@apply P y) Q)) (forall n , (implies (gt n 0) (gt -1 0)))\n\tQ (gt -1 0)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tP (@lambda v , (gt v 0))\n\t\tQ (gt -1 0)\n\t)\n)\n"
},
{
"filename": "/matching tests/test 78.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P Q)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(exists x , (@apply P x)) (exists n , (lt n a))\n\t(forall y , (implies (@apply P y) Q)) (forall a , (implies (lt a a) (lt a a)))\n\tQ (lt a a)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t// no solutions\n)\n"
},
{
"filename": "/matching tests/test 79.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// Declare the metavariables in this matching problem:\n(metavariables P y)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(exists x , (@apply P x)) (exists t , (exists p , (b t p)))\n\t(@apply P y) (exists p , (b n p))\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t(\n y n\n P (@lambda v , (exists p , (b v p)))\n )\n)\n"
},
{
"filename": "/matching tests/test 8.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P x y)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P x) (equals (plus 2 3) 5)\n\t(@apply P y) (equals 5 5)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tx (plus 2 3)\n\t\ty 5\n\t\tP (@lambda v , (equals v 5))\n\t)\n\t( // solution 2\n\t\tx (equals (plus 2 3) 5)\n\t\ty (equals 5 5)\n\t\tP (@lambda v , v)\n\t)\n)\n"
},
{
"filename": "/matching tests/test 9.putdown",
"metadata": {
"testing": {
"type": "matching"
}
},
"content": "\n// This file was autogenerated as part of an export process from an old repository.\n\n// Declare the metavariables in this matching problem:\n(metavariables P x y)\n\n// List the pattern-expression pairs in this matching problem:\n(problem\n\t(@apply P x) (A 1 2 3)\n\t(@apply P y) (A 2 1 3)\n)\n\n// List all solutions in this matching problem:\n(solutions\n\t( // solution 1\n\t\tx (A 1 2 3)\n\t\ty (A 2 1 3)\n\t\tP (@lambda v , v)\n\t)\n)\n"
},
{
"filename": "/multi-matching tests/test 1.putdown",
"metadata": {
"testing": {
"type": "multi-matching"
}
},
"content": "\n// Declare the metavariables in this multi-matching problem:\n(metavariables x y)\n\n// List the pattern-then-expressions tuples in this multi-matching problem:\n(problem\n (constraint (and x y) (and 1 2) (and 3 4) )\n (constraint (and 3 y) (and 1 4) (and 3 2) )\n)\n\n// List all solutions in this multi-matching problem:\n// (Note that each one comes with a list of indices,\n// followed by a metavariable assignment.)\n(solutions\n (0 1)\n (\n x 1\n y 2\n )\n)\n"
},
{
"filename": "/multi-matching tests/test 10.putdown",
"metadata": {
"testing": {
"type": "possible sufficient instantiations"
}
},
"content": "\n// Metavariables used in the formula below:\n(metavariables A B)\n\n// The formula to be instantiated:\n{\n :A\n :B\n (^ A B)\n}\n// Note that the above formula will become the following sequence of patterns:\n// [ A, B, (^ A B) ]\n\n// The sequent we will attempt to make true:\n{\n :X\n :(-> Y Z)\n :Y\n (^ Y X)\n}\n// Note that the above formula will become the following sequence of patterns:\n// [ X, (-> Y Z), Y, (^ Y X) ]\n\n// The options to use when searching:\n(options direct) // but still keep the default of not intuitionistic\n\n// List all solutions expected:\n// (Note that each one comes with a list of indices, followed by a metavariable\n// assignment. Negative indices indicate that the pattern in question was\n// optional and was not matched to any expression.)\n(solutions\n (-1 -1 3) (A Y B X) // instantiate just the third one\n (-1 0 3) (A Y B X) // instantiate just the second and third ones\n ( 2 -1 3) (A Y B X) // instantiate just the first and third ones\n ( 2 0 3) (A Y B X) // instantiate all 3\n)\n"
},
{
"filename": "/multi-matching tests/test 11.putdown",
"metadata": {
"testing": {
"type": "possible sufficient instantiations"
}
},
"content": "\n// Metavariables used in the formula below:\n(metavariables A B)\n\n// The formula to be instantiated:\n{\n :A\n :B\n (^ A B)\n}\n// Note that the above formula will become the following sequence of patterns:\n// [ A, B, (^ A B) ]\n\n// The sequent we will attempt to make true:\n{\n :X\n :(-> Y Z)\n :Y\n (^ Y X)\n}\n// Note that the above formula will become the following sequence of patterns:\n// [ X, (-> Y Z), Y, (^ Y X) ]\n\n// The options to use when searching:\n(options intuitionistic) // but still keep the default of not direct\n\n// List all solutions expected:\n// (Note that each one comes with a list of indices, followed by a metavariable\n// assignment. Negative indices indicate that the pattern in question was\n// optional and was not matched to any expression.)\n(solutions\n ( 2 0 3) (A Y B X) // in this case, must instantiate all three\n)\n"
},
{
"filename": "/multi-matching tests/test 12.putdown",
"metadata": {
"testing": {
"type": "possible sufficient instantiations"
}
},
"content": "\n// Metavariables used in the formula below:\n(metavariables A B)\n\n// The formula to be instantiated:\n{\n :A\n :B\n (^ A B)\n}\n// Note that the above formula will become the following sequence of patterns:\n// [ A, B, (^ A B) ]\n\n// The sequent we will attempt to make true:\n{\n :X\n :(-> Y Z)\n :Y\n (^ Y X)\n}\n// Note that the above formula will become the following sequence of patterns:\n// [ X, (-> Y Z), Y, (^ Y X) ]\n\n// The options to use when searching:\n(options intuitionistic direct)\n\n// List all solutions expected:\n// (Note that each one comes with a list of indices, followed by a metavariable\n// assignment. Negative indices indicate that the pattern in question was\n// optional and was not matched to any expression.)\n(solutions\n ( 2 0 3) (A Y B X) // in this case, must instantiate all three\n)\n"
},
{
"filename": "/multi-matching tests/test 13.putdown",
"metadata": {
"testing": {
"type": "possible sufficient instantiations"
}
},
"content": "\n// Metavariables used in the formula below:\n(metavariables P Q)\n\n// The formula to be instantiated:\n{\n :{ :P Q }\n (-> P Q)\n}\n// Note that the above formula will become the following sequence of patterns:\n// [ P, Q, (-> P Q) ]\n\n// The sequent we will attempt to make true:\n{\n :{ :X Y }\n :{ :R S }\n :Y\n (-> X Y)\n}\n// Note that the above formula will become the following sequence of patterns:\n// [ X, Y, R, S, Y, (-> X Y) ]\n// Which will then get reduced to the following, because of the duplicate Y:\n// [ X, Y, R, S, (-> X Y) ]\n\n// The options to use when searching:\n(options intuitionistic)\n// This will limit the candidates when searching to this:\n// P may optionally match any of [ X, R, (-> X Y) ]\n// Q must match one of [ Y, S, Y ]\n// (-> P Q) must match one of [ X, R, (-> X Y) ]\n\n// List all solutions expected:\n// (Note that each one comes with a list of indices, followed by a metavariable\n// assignment. Negative indices indicate that the pattern in question was\n// optional and was not matched to any expression.)\n(solutions\n (-1 1 5) (P X Q Y) // P not matched, Q=Y\n ( 0 1 5) (P X Q Y) // P=X, Q=Y\n)\n"
},
{
"filename": "/multi-matching tests/test 14.putdown",
"metadata": {
"testing": {
"type": "possible sufficient instantiations"
}
},
"content": "\n// Metavariables used in the formula below:\n(metavariables P Q)\n\n// The formula to be instantiated:\n{\n :{ :P Q }\n (-> P Q)\n}\n// Note that the above formula will become the following sequence of patterns:\n// [ P, Q, (-> P Q) ]\n\n// The sequent we will attempt to make true:\n{\n :{ :X Y }\n :{ :R S }\n :{ :F G }\n (-> X Y)\n}\n// Note that the above formula will become the following sequence of patterns:\n// [ X, Y, R, S, F, G, (-> X Y) ]\n\n// The options to use when searching:\n(options intuitionistic)\n// This will limit the candidates when searching to this:\n// P may optionally match any of [ X, R, F, (-> X Y) ]\n// Q must match one of [ Y, S, G ]\n// (-> P Q) must match one of [ X, R, F, (-> X Y) ]\n\n// List all solutions expected:\n// (Note that each one comes with a list of indices, followed by a metavariable\n// assignment. Negative indices indicate that the pattern in question was\n// optional and was not matched to any expression.)\n(solutions\n (-1 1 6) (P X Q Y) // P not matched, Q=Y\n ( 0 1 6) (P X Q Y) // P=X, Q=Y\n)\n"
},
{
"filename": "/multi-matching tests/test 2.putdown",
"metadata": {
"testing": {
"type": "multi-matching"
}
},
"content": "\n// Declare the metavariables in this multi-matching problem:\n(metavariables P t)\n\n// List the pattern-then-expressions tuples in this multi-matching problem:\n(problem\n (constraint (forall x , (@apply P x))\n (> 5 n)\n (forall k , (happier k 7))\n (forall q , (= (+ q r) t))\n (exists foo , bar) )\n (constraint (@apply P t)\n (= (+ 9 r) t) )\n)\n\n// List all solutions in this multi-matching problem:\n// (Note that each one comes with a list of indices,\n// followed by a metavariable assignment.)\n(solutions\n (2 0)\n (\n t 9\n P (@lambda v , (= (+ v r) t))\n )\n)\n"
},
{
"filename": "/multi-matching tests/test 3.putdown",
"metadata": {
"testing": {
"type": "multi-matching"
}
},
"content": "\n// Declare the metavariables in this multi-matching problem:\n(metavariables A B C)\n\n// List the pattern-then-expressions tuples in this multi-matching problem:\n(problem\n (constraint (or A B) (or p p) (=> p p) p )\n (constraint (=> A C) (or p p) (=> p p) p )\n (constraint (=> B C) (or p p) (=> p p) p )\n (constraint C (or p p) (=> p p) p )\n)\n\n// List all solutions in this multi-matching problem:\n// (Note that each one comes with a list of indices,\n// followed by a metavariable assignment.)\n(solutions\n (0 1 1 2)\n (\n A p\n B p\n C p\n )\n)\n"
},
{
"filename": "/multi-matching tests/test 4.putdown",
"metadata": {
"testing": {
"type": "multi-matching"
}
},
"content": "\n// Declare the metavariables in this multi-matching problem:\n(metavariables a b P)\n\n// List the pattern-then-expressions tuples in this multi-matching problem:\n(problem\n (constraint (= a b)\n (> (squared 5) (squared x))\n (= (+ 3 1) 4)\n (= x 4)\n (= y 3) )\n (constraint (@apply P a)\n (> (squared 5) (squared x))\n (= (+ 3 1) 4)\n (= x 4)\n (= y 3) )\n (constraint (@apply P b)\n (> (squared 5) (squared 4)) )\n)\n\n// List all solutions in this multi-matching problem:\n// (Note that each one comes with a list of indices,\n// followed by a metavariable assignment.)\n(solutions\n (2 0 0)\n (\n a x\n b 4\n P (@lambda v , (> (squared 5) (squared v)))\n )\n)\n"
},
{
"filename": "/multi-matching tests/test 5.putdown",
"metadata": {
"testing": {
"type": "multi-matching"
}
},
"content": "\n// Imagine that we wish to use the multi-matching algorithm to look for\n// instantiations of the equality elimination rule that will make a certain\n// conclusion true, by searching among the accessible premises. Here is a\n// small example document.\n//\n// {\n// :{ :(= a b) :(@apply P a) (@apply P b) } // the formula\n// (^ (= 1 2) (= 2 3)) // not an =-type expression\n// (= 1 2) // possible =-type premise\n// (= 2 3) // possible =-type premise\n// (> 1 3) // not an =-type expression\n// (= 1 3) // desired conclusion\n// }\n//\n// We would set up a multi-matching problem as follows:\n// - one of the 4 usable premises must match (= a b)\n// - one of the 4 usable premises must match (@apply P a)\n// - the conclusion (= 1 3) must match (@apply P b)\n// We do exactly that below.\n\n// Declare the metavariables in this optional multi-matching problem:\n(metavariables a b P)\n\n// List the pattern-then-expressions tuples in this multi-matching problem:\n(problem\n (constraint (= a b) (^ (= 1 2) (= 2 3)) (= 1 2) (= 2 3) (> 1 3) )\n (constraint (@apply P a) (^ (= 1 2) (= 2 3)) (= 1 2) (= 2 3) (> 1 3) )\n (constraint (@apply P b) (= 1 3) )\n)\n\n// List all solutions in this multi-matching problem:\n// (Note that each one comes with a list of indices,\n// followed by a metavariable assignment.)\n(solutions\n (2 1 0)\n (\n a 2\n b 3\n P (@lambda v , (= 1 v))\n )\n)\n"
},
{
"filename": "/multi-matching tests/test 6.putdown",
"metadata": {
"testing": {
"type": "optional multi-matching"
}
},
"content": "\n// Declare the metavariables in this optional multi-matching problem:\n(metavariables x y)\n\n// List the pattern-then-expressions tuples in this multi-matching problem:\n// (Note that once one is marked \"optional,\" all later ones are optional also.)\n(problem\n (constraint (and x y) (and 1 2) (and 3 4) )\n (constraint (and 3 y) (and 1 4) (and 3 2) )\n (constraint x optional totally_unrelated_thing )\n)\n\n// List all solutions in this optional multi-matching problem:\n// (Note that each one comes with a list of indices,\n// followed by a metavariable assignment. Negative indices indicate that the\n// pattern in question was optional and was not matched to any expression.)\n(solutions\n // The only way to match this is to satisfy constraints 1 and 2 in the only\n // way that they can be satisfied, and ignore constraint 3, which cannot be\n // satisfied together with the other ones.\n (0 1 -1)\n (\n x 1\n y 2\n )\n)\n"
},
{
"filename": "/multi-matching tests/test 7.putdown",
"metadata": {
"testing": {
"type": "optional multi-matching"
}
},
"content": "\n// Declare the metavariables in this optional multi-matching problem:\n(metavariables x y)\n\n// List the pattern-then-expressions tuples in this multi-matching problem:\n// (Note that once one is marked \"optional,\" all later ones are optional also.)\n(problem\n (constraint (and x y) (and 1 2) (and 3 4) )\n (constraint (and 3 y) optional (and 1 4) (and 3 2) )\n)\n\n// List all solutions in this optional multi-matching problem:\n// (Note that each one comes with a list of indices,\n// followed by a metavariable assignment. Negative indices indicate that the\n// pattern in question was optional and was not matched to any expression.)\n(solutions\n // Full match, not using the \"optional\" flag on constraint 2\n (0 1)\n (\n x 1\n y 2\n )\n // Same assignment as previous, but now ignoring constraint 2\n (0 -1)\n (\n x 1\n y 2\n )\n // Different assignment than #1, because we don't have constraint 2\n (1 -1)\n (\n x 3\n y 4\n )\n)\n"
},
{
"filename": "/multi-matching tests/test 8.putdown",
"metadata": {
"testing": {
"type": "optional multi-matching"
}
},
"content": "\n// Imagine that we wish to use the optional multi-matching algorithm to look\n// for instantiations of the equality elimination rule that will make a certain\n// conclusion true, by searching among the accessible premises. Here is a\n// small example document.\n//\n// {\n// :{ :{ :A B } (=> A B) } // the formula\n// { // the only environment premise\n// :(hello there) // instantiation of A\n// hi! // possible instantiation of B\n// (how r u?) // another possible instantiation of B\n// }\n// bar // the premise we will actually use\n// (=> foo bar) // the desired conclusion\n// }\n//\n// We would set up an optional multi-matching problem as follows:\n// - A must match (hello there) if it matches anything, but it's optional\n// - B must match one of: hi!, (how r u?), bar\n// - (=> A B) must match the desired conclusion (=> foo bar)\n// We do exactly that below.\n\n// Declare the metavariables in this optional multi-matching problem:\n(metavariables A B)\n\n// List the pattern-then-expressions tuples in this multi-matching problem:\n// (Note that once one is marked \"optional,\" all later ones are optional also.)\n(problem\n (constraint B hi! (how r u?) bar )\n (constraint (=> A B) (=> foo bar) )\n (constraint A optional (hello there) )\n)\n\n// List all solutions in this optional multi-matching problem:\n// (Note that each one comes with a list of indices,\n// followed by a metavariable assignment. Negative indices indicate that the\n// pattern in question was optional and was not matched to any expression.)\n(solutions\n (2 0 -1)\n (\n A foo\n B bar\n )\n)\n"
},
{
"filename": "/multi-matching tests/test 9.putdown",
"metadata": {
"testing": {
"type": "possible sufficient instantiations"
}
},
"content": "\n// Metavariables used in the formula below:\n(metavariables A B)\n\n// The formula to be instantiated:\n{\n :A\n :B\n (^ A B)\n}\n// Note that the above formula will become the following sequence of patterns:\n// [ A, B, (^ A B) ]\n\n// The sequent we will attempt to make true:\n{\n :X\n :(-> Y Z)\n :Y\n (^ Y X)\n}\n// Note that the above formula will become the following sequence of patterns:\n// [ X, (-> Y Z), Y, (^ Y X) ]\n\n// The options to use when searching:\n(options none) // defaults: not direct, not intuitionistic\n\n// List all solutions expected:\n// (Note that each one comes with a list of indices, followed by a metavariable\n// assignment. Negative indices indicate that the pattern in question was\n// optional and was not matched to any expression.)\n(solutions\n // 1 way to instantiate none of the formula's outermost expressions\n (-1 -1 -1) empty_function\n // 1 way to instantiate just the third one\n (-1 -1 3) (A Y B X)\n // 4 ways to instantiate just the second one\n (-1 0 -1) (B X)\n (-1 1 -1) (B (-> Y Z))\n (-1 2 -1) (B Y)\n (-1 3 -1) (B (^ Y X))\n // 1 way to instantiate just the second and third ones\n (-1 0 3) (A Y B X)\n // 4 ways to instantiate just the first one\n ( 0 -1 -1) (A X)\n ( 1 -1 -1) (A (-> Y Z))\n ( 2 -1 -1) (A Y)\n ( 3 -1 -1) (A (^ Y X))\n // 1 way to instantiate just the first and third ones\n ( 2 -1 3) (A Y B X)\n // 16 ways to instantiate just the first and second ones\n ( 0 0 -1) (A X B X)\n ( 0 1 -1) (A X B (-> Y Z))\n ( 0 2 -1) (A X B Y)\n ( 0 3 -1) (A X B (^ Y X))\n ( 1 0 -1) (A (-> Y Z) B X)\n ( 1 1 -1) (A (-> Y Z) B (-> Y Z))\n ( 1 2 -1) (A (-> Y Z) B Y)\n ( 1 3 -1) (A (-> Y Z) B (^ Y X))\n ( 2 0 -1) (A Y B X)\n ( 2 1 -1) (A Y B (-> Y Z))\n ( 2 2 -1) (A Y B Y)\n ( 2 3 -1) (A Y B (^ Y X))\n ( 3 0 -1) (A (^ Y X) B X)\n ( 3 1 -1) (A (^ Y X) B (-> Y Z))\n ( 3 2 -1) (A (^ Y X) B Y)\n ( 3 3 -1) (A (^ Y X) B (^ Y X))\n // 1 way to instantiate all 3\n ( 2 0 3) (A Y B X)\n)\n"
},
{
"filename": "/parsing tests/syntax error 1.putdown",
"metadata": {
"testing": {
"syntax": "invalid"
}
},
"content": "\n// This file contains an Expression with an Environment inside, which is\n// invalid putdown syntax.\n\n(+ 1 2 { :A B })\n"
},
{
"filename": "/parsing tests/syntax error 2.putdown",
"metadata": {
"testing": {
"syntax": "invalid"
}
},
"content": "\n{* A B C *} // invalid because we deleted formula notation\n"
},
{
"filename": "/parsing tests/valid syntax 1.putdown",
"metadata": {
"testing": {
"syntax": "valid",
"length": 4
}
},
"content": "\n// This file contains several Expressions, all using valid putdown notation.\n\n(+ 1 2)\n\n(- k t (* u v))\n\n(polynomial (variable x) (coefficients 9 0 -6 2 1))\n\n(forall x , (exists y , (> x y)))\n"
},
{
"filename": "/parsing tests/valid syntax 2.putdown",
"metadata": {
"testing": {
"syntax": "valid",
"length": 1
}
},
"content": "\n// This file contains some nested Environments, Expressions, and Declarations,\n// all using valid putdown syntax.\n\n{\n // Let x be arbitrary.\n [x]\n // Assume x is a real number.\n :(in x R)\n // Claim that x is a complex number, by Theorem 21\n (in x C) +{\"reason\":\"Theorem 21\"}\n}\n"
},
{
"filename": "/parsing tests/syntax error 1.smackdown",
"metadata": {
"testing": {
"syntax": "invalid"
}
},
"content": "\n// This file contains an Expression with an Environment inside, which is\n// invalid smackdown syntax, because it is invalid putdown syntax.\n\n(+ 1 2 { :A B })\n"
},
{
"filename": "/parsing tests/syntax error 2.smackdown",
"metadata": {
"testing": {
"syntax": "invalid"
}
},
"content": "\n\\label{hello} // invalid because it is preceded by no LC to modify\n(one two three)\n"
},
{
"filename": "/parsing tests/valid syntax 1.smackdown",
"metadata": {
"testing": {
"syntax": "valid",
"length": 3
}
},
"content": "\n// This file contains several examples of valid smackdown expressions\n\n(+ 1 2) // valid putdown\n\n$k-t-u*v$ // a smackdown \"notation\" atom (for later parsing)\n\n(forall x , (exists y , $x>y$)) // smackdown inside putdown is also valid\n"
},
{
"filename": "/parsing tests/valid syntax 2.smackdown",
"metadata": {
"testing": {
"syntax": "valid",
"length": 1
}
},
"content": "\n// This file contains more complex smackdown, including labels,\n// references, and proof markers.\n\n\\begin{proof}\n // Let x be arbitrary and mark it with label \"1\"\n [x] \\label{1}\n // Assume x is a real number and mark it with label \"2\"\n :$x∈R$ \\label{2}\n // Claim that x is a complex number, by Theorem 21\n $x∈C$ \\reason{Theorem 21}\n // (Even though no reason command has a built-in meaning implemented,\n // smackdown will still parse it and remember it was a command.)\n\\end{proof}\n"
},
{
"filename": "/propositional logic/all rules.putdown",
"metadata": {
"includes": [
"declare connectives.putdown",
"conjunction introduction.putdown",
"conjunction elimination.putdown",
"disjunction introduction.putdown",
"disjunction elimination.putdown",
"conditional introduction.putdown",
"conditional elimination.putdown",
"negation introduction.putdown",
"negation elimination.putdown",
"biconditional introduction.putdown",
"biconditional elimination.putdown"
]
},
"content": "\n// Declare the logical connectives as constants:\n\n[and or not implies iff const]\n\n\n{\n :A\n :B\n (and A B)\n}\n\n\n{\n :(and A B)\n A\n B\n}\n\n\n{\n :A\n (or A B)\n}\n\n{\n :B\n (or A B)\n}\n\n\n{\n :(or A B)\n :(implies A C)\n :(implies B C)\n C\n}\n\n\n{\n :{\n :A\n B\n }\n (implies A B)\n}\n\n\n{\n :(implies A B)\n :A\n B\n}\n\n\n{\n :{\n :A\n B\n (not B)\n }\n (not A)\n}\n\n\n{\n :{\n :(not A)\n B\n (not B)\n }\n A\n}\n\n\n{\n :{\n :A\n B\n }\n :{\n :B\n A\n }\n (iff A B)\n}\n\n\n{\n :(iff A B)\n :A\n B\n}\n\n{\n :(iff A B)\n :B\n A\n}\n\n",
"original": ""
},
{
"filename": "/propositional logic/biconditional elimination.putdown",
"metadata": {
"rule": true,
"names": [
"biconditional elimination",
"<->E"
]
},
"content": "\n{\n :(iff A B)\n :A\n B\n}\n\n{\n :(iff A B)\n :B\n A\n}\n"
},
{
"filename": "/propositional logic/biconditional introduction.putdown",
"metadata": {
"rule": true,
"names": [
"conditional introduction",
"->I"
]
},
"content": "\n{\n :{\n :A\n B\n }\n :{\n :B\n A\n }\n (iff A B)\n}\n"
},
{
"filename": "/propositional logic/conditional elimination.putdown",
"metadata": {
"rule": true,
"names": [
"conditional elimination",
"->E"
]
},
"content": "\n{\n :(implies A B)\n :A\n B\n}\n"
},
{
"filename": "/propositional logic/conditional introduction.putdown",
"metadata": {
"rule": true,
"names": [
"conditional introduction",
"->I"
]
},
"content": "\n{\n :{\n :A\n B\n }\n (implies A B)\n}\n"
},
{
"filename": "/propositional logic/conjunction elimination.putdown",
"metadata": {
"rule": true,
"names": [
"conjunction elimination",
"^E"
]
},
"content": "\n{\n :(and A B)\n A\n B\n}\n"
},
{
"filename": "/propositional logic/conjunction introduction.putdown",
"metadata": {
"rule": true,
"names": [
"conjunction introduction",
"^I"
]
},
"content": "\n{\n :A\n :B\n (and A B)\n}\n"
},
{
"filename": "/propositional logic/declare connectives.putdown",
"metadata": {},
"content": "\n// Declare the logical connectives as constants:\n\n[and or not implies iff const]\n"
},
{
"filename": "/propositional logic/disjunction elimination.putdown",
"metadata": {
"rule": true,
"names": [
"disjunction elimination",
"vE"
]
},
"content": "\n{\n :(or A B)\n :(implies A C)\n :(implies B C)\n C\n}\n"
},
{
"filename": "/propositional logic/disjunction introduction.putdown",
"metadata": {
"rule": true,
"names": [
"disjunction introduction",
"vI"
]
},
"content": "\n{\n :A\n (or A B)\n}\n\n{\n :B\n (or A B)\n}\n"
},
{
"filename": "/propositional logic/negation elimination.putdown",
"metadata": {
"rule": true,
"names": [
"negation elimination",
"-E"
]
},
"content": "\n{\n :{\n :(not A)\n B\n (not B)\n }\n A\n}\n"
},
{
"filename": "/propositional logic/negation introduction.putdown",
"metadata": {
"rule": true,
"names": [
"negation introduction",
"-I"
]
},
"content": "\n{\n :{\n :A\n B\n (not B)\n }\n (not A)\n}\n"
},
{
"filename": "/validation tests/prop test 01.putdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "propositional"
},
"imported": {
"source": "fic-experiment repository",
"file": "scripts/init.js",
"name": "BadLC"
}
},
"content": "\n{\n :{\n :W\n :V\n U\n V\n }\n :W\n :V\n U +{\"expected validation result\":\"valid\"}\n}\n"
},
{
"filename": "/validation tests/prop test 02.putdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "propositional"
},
"imported": {
"source": "fic-experiment repository",
"file": "scripts/init.js",
"name": "imp2"
}
},
"content": "\n{\n :{\n A\n :B\n }\n A +{\"expected validation result\":\"valid\"}\n :C\n C +{\"expected validation result\":\"valid\"}\n}\n"
},
{
"filename": "/validation tests/prop test 03.putdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "propositional"
},
"imported": {
"source": "fic-experiment repository",
"file": "test/data/PropProofsTxt.js"
}
},
"content": "\n{\n :{\n :{\n W\n V\n }\n (and W V)\n (and V W)\n }\n :{\n :(and W V)\n W\n V\n }\n :{\n :W\n (or W V)\n (or V W)\n }\n :{\n :(or W V)\n :{\n :W\n R\n }\n :{\n :W\n R\n }\n R\n }\n :{\n :{\n :W\n V\n }\n (implies W V)\n }\n :{\n :W\n :(implies W V)\n V\n }\n :{\n :{\n :W\n V\n }\n :{\n :V\n W\n }\n (iff W V)\n }\n :{\n :(iff W V)\n {\n :V\n W\n }\n {\n :W\n V\n }\n }\n :{\n :{\n :W\n contradiction\n }\n (not W)\n }\n :{\n :{\n :(not W)\n contradiction\n }\n W\n }\n :{\n :W\n :(not W)\n contradiction\n }\n :{\n :(not P)\n (or P (not P))\n }\n :{\n :P\n (or P (not P))\n }\n :{\n :P\n (or P Q)\n }\n :{\n :Q\n (or P Q)\n }\n :{\n :(or P Q)\n (or (or P Q) R)\n }\n :{\n :R\n (or (or P Q) R)\n }\n :{\n :P\n (or P (and (not P) P))\n }\n :{\n :(not P)\n (or (not P) (not Q))\n }\n :{\n :(not Q)\n (or (not P) (not Q))\n }\n :{\n :(or Q R)\n :{\n :Q\n (or (or P Q) R)\n }\n :{\n :R\n (or (or P Q) R)\n }\n (or (or P Q) R)\n }\n :{\n :(or P (or Q R))\n :{\n :P\n (or (or P Q) R)\n }\n :{\n :(or Q R)\n (or (or P Q) R)\n }\n (or (or P Q) R)\n }\n :{\n :(or (not P) (not Q))\n :{\n :(not P)\n contradiction\n }\n :{\n :(not Q)\n contradiction\n }\n contradiction\n }\n :{\n :(or P (not P))\n :(not (or P (not P)))\n contradiction\n }\n :{\n :(not (or (not P) (not Q)))\n :(or (not P) (not Q))\n contradiction\n }\n :{\n :(not (and P Q))\n :(and P Q)\n contradiction\n }\n :{\n :(not P)\n :P\n contradiction\n }\n :{\n :(not Q)\n :Q\n contradiction\n }\n :{\n :{\n :(not P)\n contradiction\n }\n P\n }\n :{\n :{\n :(not Q)\n contradiction\n }\n Q\n }\n :{\n :{\n :(not (or P (not P)))\n contradiction\n }\n (or P (not P))\n }\n :{\n :{\n :(not (or (not P) (not Q)))\n contradiction\n }\n (or (not P) (not Q))\n }\n :{\n :{\n :(and P Q)\n contradiction\n }\n (not (and P Q))\n }\n :{\n :{\n :contradiction\n P\n }\n (implies contradiction P)\n }\n :{\n :{\n :(or P (or Q R))\n (or (or P Q) R)\n }\n (implies (or P (or Q R)) (or (or P Q) R))\n }\n :{\n :{\n :P\n (or P (and (not P) P))\n }\n (implies P (or P (and (not P) P)))\n }\n :{\n :{\n :(or P (and (not P) P))\n P\n }\n (implies (or P (and (not P) P)) P)\n }\n :{\n :{\n :P\n (iff P (or P (and (not P) P)))\n }\n (implies P (iff P (or P (and (not P) P))))\n }\n :{\n :{\n :(not (and P Q))\n (or (not P) (not Q))\n }\n (implies (not (and P Q)) (or (not P) (not Q)))\n }\n :{\n :{\n :(or (not P) (not Q))\n (not (and P Q))\n }\n (implies (or (not P) (not Q)) (not (and P Q)))\n }\n :{\n :(implies P (or P (and (not P) P)))\n :(implies (or P (and (not P) P)) P)\n (iff P (or P (and (not P) P)))\n }\n :{\n :(implies (not (and P Q)) (or (not P) (not Q)))\n :(implies (or (not P) (not Q)) (not (and P Q)))\n (iff (not (and P Q)) (or (not P) (not Q)))\n }\n :{\n :P\n :Q\n (and P Q)\n }\n :{\n :P\n :Q\n (and P Q)\n }\n :{\n :(and P Q)\n P\n Q\n }\n {\n :(not (or P (not P)))\n {\n :(not P)\n (or P (not P)) +{\"expected validation result\":\"valid\"}\n contradiction +{\"expected validation result\":\"valid\"}\n }\n P +{\"expected validation result\":\"valid\"}\n (or P (not P)) +{\"expected validation result\":\"valid\"}\n contradiction +{\"expected validation result\":\"valid\"}\n }\n (or P (not P)) +{\"expected validation result\":\"valid\"}\n {\n :contradiction\n {\n :(not P)\n contradiction +{\"expected validation result\":\"valid\"}\n }\n P +{\"expected validation result\":\"valid\"}\n }\n (implies contradiction P) +{\"expected validation result\":\"valid\"}\n {\n :(or P (or Q R))\n {\n :P\n (or P Q) +{\"expected validation result\":\"valid\"}\n (or (or P Q) R) +{\"expected validation result\":\"valid\"}\n }\n {\n :(or Q R)\n {\n :Q\n (or P Q) +{\"expected validation result\":\"valid\"}\n (or (or P Q) R) +{\"expected validation result\":\"valid\"}\n }\n {\n :R\n (or (or P Q) R) +{\"expected validation result\":\"valid\"}\n }\n (or (or P Q) R) +{\"expected validation result\":\"valid\"}\n }\n (or (or P Q) R) +{\"expected validation result\":\"valid\"}\n }\n (implies (or P (or Q R)) (or (or P Q) R)) +{\"expected validation result\":\"valid\"}\n {\n :P\n {\n :P\n (or P (and (not P) P)) +{\"expected validation result\":\"valid\"}\n }\n (implies P (or P (and (not P) P))) +{\"expected validation result\":\"valid\"}\n {\n :(or P (and (not P) P))\n P +{\"expected validation result\":\"valid\"}\n }\n (implies (or P (and (not P) P)) P) +{\"expected validation result\":\"valid\"}\n (iff P (or P (and (not P) P))) +{\"expected validation result\":\"valid\"}\n }\n (implies P (iff P (or P (and (not P) P)))) +{\"expected validation result\":\"valid\"}\n {\n :(not (and P Q))\n {\n :(not (or (not P) (not Q)))\n {\n :(not P)\n (or (not P) (not Q)) +{\"expected validation result\":\"valid\"}\n contradiction +{\"expected validation result\":\"valid\"}\n }\n P +{\"expected validation result\":\"valid\"}\n {\n :(not Q)\n (or (not P) (not Q)) +{\"expected validation result\":\"valid\"}\n contradiction +{\"expected validation result\":\"valid\"}\n }\n Q +{\"expected validation result\":\"valid\"}\n (and P Q) +{\"expected validation result\":\"valid\"}\n contradiction +{\"expected validation result\":\"valid\"}\n }\n (or (not P) (not Q)) +{\"expected validation result\":\"valid\"}\n }\n (implies (not (and P Q)) (or (not P) (not Q))) +{\"expected validation result\":\"valid\"}\n {\n :(or (not P) (not Q))\n {\n :(and P Q)\n P +{\"expected validation result\":\"valid\"}\n Q +{\"expected validation result\":\"valid\"}\n {\n :(not P)\n contradiction +{\"expected validation result\":\"valid\"}\n }\n {\n :(not Q)\n contradiction +{\"expected validation result\":\"valid\"}\n }\n contradiction +{\"expected validation result\":\"valid\"}\n }\n (not (and P Q)) +{\"expected validation result\":\"valid\"}\n }\n (implies (or (not P) (not Q)) (not (and P Q))) +{\"expected validation result\":\"valid\"}\n (iff (not (and P Q)) (or (not P) (not Q))) +{\"expected validation result\":\"valid\"}\n}\n"
},
{
"filename": "/validation tests/prop test 04.putdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "propositional"
}
},
"content": "\n{\n :{\n :G\n {\n :A\n B\n }\n }\n {\n :G\n :A\n B +{\"expected validation result\":\"valid\"}\n }\n}\n"
},
{
"filename": "/validation tests/prop test 05.putdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "propositional"
}
},
"content": "\n{\n :{\n :{\n :A\n B\n }\n {\n :A\n C\n }\n }\n {\n :{\n :B\n C\n }\n C +{\"expected validation result\":\"invalid\"}\n }\n}\n"
},
{
"filename": "/validation tests/prop test 06.putdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "propositional"
}
},
"content": "\n{\n :{ :A B }\n :{ :C D }\n :{ :E F }\n :{ :G H }\n :{ :I J }\n :{ :K L }\n :{ M N }\n :{ :O P }\n :{ :Q R }\n :{ :R A }\n :{ :P C }\n :{ :N E }\n :{ :L G }\n :{ :I E }\n :{ :K F }\n :{ :M G }\n :{ :O H }\n :{ :Q I }\n A +{\"expected validation result\":\"invalid\"}\n}\n"
},
{
"filename": "/validation tests/blatant instantiation hint 01.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "blatant instantiation hint",
"description": "Basic test of a blatant instantiation hint"
}
},
"content": "\n(⇒ ¬ or),{\n \n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n \n // blatant instantiation hint\n { :(⇒ A B) (or (¬ A) B) \\valid } \\ref{alt def of ⇒} \\valid\n \n // start a proof\n {\n :(⇒ A B)\n (or (¬ A) B) \\valid\n }\n\n}\n"
},
{
"filename": "/validation tests/blatant instantiation hint 02.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "blatant instantiation hint",
"description": "A valid instantiation, but the formula is inaccessible (and meaningless)"
}
},
"content": "\n(⇒ ¬ or),{\n {\n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n }\n \n // blatant instantiation hint\n // Note, if it is a valid instantation, but the formula is inaccessible\n // we mark the BIH tool as \\valid, but the conclusion as invalid:\n { :(⇒ A B) (or (¬ A) B) \\invalid } \\ref{alt def of ⇒} \\invalid\n \n // start a proof\n {\n :(⇒ A B)\n (or (¬ A) B) \\valid\n }\n\n}\n"
},
{
"filename": "/validation tests/blatant instantiation hint 03.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "blatant instantiation hint",
"description": "A valid instantiation, but not the one needed to justify the conclusion"
}
},
"content": "\n(⇒ ¬ or),{\n\n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n \n // blatant instantiation hint\n :{ :(⇒ A A) (or (¬ A) A) \\valid } \\ref{alt def of ⇒} \\valid\n\n // start a proof\n {\n :(⇒ A B)\n (or (¬ A) B) \\invalid\n }\n\n}\n"
},
{
"filename": "/validation tests/blatant instantiation hint 04.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "blatant instantiation hint",
"description": "Citing the wrong formula"
}
},
"content": "\n(⇒ ¬ or),{\n\n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n :{ (⇒ P P) } \\label{reflexive of ⇒}\n\n // blatant instantiation hint\n { :(⇒ A B) (or (¬ A) B) \\invalid } \\ref{reflexive of ⇒} \\invalid\n // start a proof\n {\n :(⇒ A B)\n (or (¬ A) B) \\valid\n }\n\n}\n"
},
{
"filename": "/validation tests/blatant instantiation hint 05.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "blatant instantiation hint",
"description": "A valid instantiation, but the formula is inaccessible"
}
},
"content": "\n(⇒ ¬ or),{\n \n // blatant instantiation hint\n :{ :(⇒ A B) (or (¬ A) B) \\invalid } \\ref{reflexive of ⇒} \\invalid\n\n // start a proof\n {\n :(⇒ A B)\n (or (¬ A) B) \\valid\n }\n \n // too late\n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n\n}\n"
},
{
"filename": "/validation tests/blatant instantiation hint 06.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "blatant instantiation hint",
"description": "Natural Deduction Propositional Proof of (P⇒P)"
}
},
"content": "\n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // blatant instantiation hint\n { :{:P P} (⇒ P P) \\valid } \\ref{⇒+} \\valid\n \n // Theorem (notice we get this for free .. we don't even need the proof)\n (⇒ P P) \\valid\n \n // Baby warm up proof... just for kicks\n {\n { :P \n P \\valid\n }\n (⇒ P P) \\valid\n }\n \n}\n"
},
{
"filename": "/validation tests/blatant instantiation hint 07.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "blatant instantiation hint",
"description": "Natural Deduction Propositional Proof (alt or-)"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇔ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n // blatant instantiation hints\n { :{ :(¬ P) Q (¬ Q)} P \\valid } \\ref{¬-} \\valid\n { :(∨ P Q) :{ :P P } :{:Q P} P \\valid } \\ref{∨-} \\valid\n \n // Theorem (alt or-)\n { :(∨ P Q) :(¬ Q) P \\valid }\n\n // Altertnate or- proof (not needed but motivates the instantiations\n {\n { :(∨ P Q) \n :(¬ Q)\n { :P\n P \\valid // no instantiation needed\n }\n { :Q\n { :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\valid // motivates ¬- instantiation\n }\n P \\valid // motivates or- instantiation\n }\n }\n\n}\n"
},
{
"filename": "/validation tests/blatant instantiation hint 08.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "blatant instantiation hint",
"description": "Natural Deduction proof using the Identity Instantiation. So only one of the instantiations in the previous test should be needed."
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // blatant instantiation hints\n { :(∨ W V) :{ :W W } :{:V W} W \\valid } \\ref{∨-} \\valid\n\n // Theorem\n { :(∨ W V) :(¬ V) W \\valid }\n \n // Altertnate or- proof\n {\n { :(∨ W V) :(¬ V)\n { :W\n W \\valid\n }\n { :V\n { :(¬ W)\n (¬ V) \\valid\n }\n W \\valid\n }\n W \\valid\n }\n }\n\n}\n"
},
{
"filename": "/validation tests/blatant instantiation hint 09.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "blatant instantiation hint",
"description": "Testing Pierce."
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n // blatant instantiation hints\n { :{:(¬ Q) P (¬ P)} Q \\valid } \\ref{¬-} \\valid\n { :{:P Q} (⇒ P Q ) \\valid } \\ref{⇒+} \\valid\n { :(⇒ P Q ) :(⇒ (⇒ P Q) P) P \\valid } \\ref{⇒-} \\valid\n { :{:(¬ P) P (¬ P)} P \\valid } \\ref{¬-} \\valid\n { :{ :(⇒ (⇒ P Q) P) P } (⇒ (⇒ (⇒ P Q) P) P) \\valid } \\ref{⇒+} \\valid\n\n // Theorem (Pierce) \n { (⇒ (⇒ (⇒ P Q) P) P) \\valid }\n\n // proof\n { \n { :(⇒ (⇒ P Q) P)\n { :(¬ P)\n { :P\n Q \\valid // motivates ¬-\n } \n (⇒ P Q) \\valid // motivates ⇒+\n P \\valid // motivates ⇒-\n }\n P \\valid // motivates second ¬-\n }\n (⇒ (⇒ (⇒ P Q) P) P) \\valid // motivates second ⇒+\n }\n\n}\n"
},
{
"filename": "/validation tests/blatant instantiation hint 10.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "blatant instantiation hint",
"description": "Natural Deduction - extra instantiations don't hurt"
}
},
"content": "\n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-} \n\n // blatant instantiation hints\n { :{:P P} (⇒ P P) \\valid } \\ref{⇒+} \\valid\n { :{:Z V} (⇒ Z V) \\valid } \\ref{⇒+} \\valid\n { :Z :Q (∧ Z Q) \\valid } \\ref{∧+} \\valid\n\n // Theorem (notice we get this for free .. we don't even need the proof)\n (⇒ P P) \\valid\n \n // Baby warm up proof... just for kicks\n {\n { :P \n P \\valid\n }\n (⇒ P P) \\valid\n }\n \n}\n"
},
{
"filename": "/validation tests/blatant instantiation hint 11.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "blatant instantiation hint",
"description": "ND using a Theorem as a Formula"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n // Corollary: (should be invalid here)\n { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) \\invalid } \n \n // blatant instantiation hints\n { :{ :(¬ P) Q (¬ Q)} P \\valid } \\ref{¬-} \\valid\n { :(∨ P Q) :{ :P P } :{:Q P} P \\valid } \\ref{∨-} \\valid\n // this is too soon for an instantiation hint\n // but the conclusion inside will be valid, using the Corollary above\n { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) \\valid } \\ref{alt or-} \\invalid\n \n // Theorem (alt or-)\n { :(¬ Q) :(∨ P Q) P \\valid } \\label{alt or-}\n\n // Alternate or- proof (not needed but motivates the instantiations\n {\n { :(∨ P Q)\n :(¬ Q)\n { :P\n P \\valid // no instantiation needed\n }\n { :Q\n { :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\valid // motivates ¬- instantiation\n }\n P \\valid // motivates or- instantiation\n }\n }\n\n}\n"
},
{
"filename": "/validation tests/blatant instantiation hint 12.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "blatant instantiation hint",
"description": "ND using a Theorem as a Formula"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n // blatant instantiation hints\n { :{ :(¬ P) Q (¬ Q)} P \\valid } \\ref{¬-} \\valid\n { :(∨ P Q) :{ :P P } :{:Q P} P \\valid } \\ref{∨-} \\valid\n // this is too soon for an instantiation hint\n { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) \\invalid } \\ref{alt or-} \\invalid\n \n // Theorem (alt or-)\n { :(¬ Q) :(∨ P Q) P \\valid } \\label{alt or-}\n\n // Alternate or- proof (not needed but motivates the instantiations\n {\n { :(∨ P Q)\n :(¬ Q)\n { :P\n P \\valid // no instantiation needed\n }\n { :Q\n { :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\valid // motivates ¬- instantiation\n }\n P \\valid // motivates or- instantiation\n }\n\n // now a blatant instantiation hint for the theorem\n { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) \\valid } \\ref{alt or-} \\valid\n\n }\n\n}\n"
},
{
"filename": "/validation tests/blatant instantiation hint 13.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "blatant instantiation hint",
"description": "ND using a Theorem as a Formula"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n // blatant instantiation hints\n { :{ :(¬ P) Q (¬ Q)} P \\valid } \\ref{¬-} \\valid\n { :(∨ P Q) :{ :P P } :{:Q P} P \\valid } \\ref{∨-} \\valid\n \n // Theorem (alt or-)\n { :(¬ Q) :(∨ P Q) P \\valid } \\label{alt or-}\n\n // Alternate or- proof (not needed but motivates the instantiations\n {\n { :(∨ P Q)\n :(¬ Q)\n { :P\n P \\valid // no instantiation needed\n }\n { :Q\n { :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\valid // motivates ¬- instantiation\n }\n P \\valid // motivates or- instantiation\n }\n\n // now a blatant instantiation hint for the theorem\n { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) \\valid } \\ref{alt or-} \\valid\n\n // Corollary:\n { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) \\valid }\n }\n\n}\n"
},
{
"filename": "/validation tests/formula test 01.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "formula",
"description": "Testing various errors in instantiation-hint blocks."
}
},
"content": "\n// Each of test of type: validation and subtype: formula begins with a\n// 'document' LC (and environment in smackdown notation) followed by sequence\n// of instantiation specifiers each of which give the necessary information to\n// construct an instatiation of a formula in the document. \n// \n// In addition to putdown notation, the document can contain smackdown commands\n// (though here we do not show them with their initial backslash, so as not to\n// confuse the smackdown parser, which is not currently smart enough to skip\n// comment lines):\n//\n// label{abc} - labels the preceding LC with 'abc'\n// valid, invalid - indicates whether the preceding LC should be \n// valid or invalid after validation\n//\n// The instantiation specifiers specify the following items:\n//\n// (formula abc) - formula to instantiate has label 'abc' \n// ((P A) (Q B)) - instantiate metavars P and Q with A and B resp. \n// (result \"valid\") - whether or not the instantiation was successfully \n// constructed \n// (reason \"foo\") - if it was unable to construct the instantiation\n// give a reason why it failed\n//\n// To process these tests, first the test will\n// 1. Construct the LC of the document form the first section.\n// a. label commands assign labels to the appropriate LCs\n// b. valid, invalid commands assign expected validation result\n// to each conclusion to check later against the actual validation\n// result.\n// 2. For each instantiation specifier it attempts to construct the\n// instantiation of the specified formula using the specified values.\n// a. If it succeeds (and was expected to), it inserts that LC into the\n// document after the formula.\n// b. If not, it checks that it failed for the expected reason\n// 3. After all instantiations are constructed and inserted, all of the \n// conclusions in the document are validated propositionally, and the\n// result of the validation checked for each conclusion to see if it \n// matches what was expected as specified by the \\valid and \\invalid \n// smackdown commands in the document.\n\n// document\n\n(⇒ ¬ or),{ // declare non-metavars\n \n :{ :(⇒ P Q) (or (¬ P) Q) } // a theorem turned formula\n \\label{alt def of ⇒} // smackdown label \n \n // start a proof\n { \n :(⇒ A B) // assume something\n (or (¬ A) B) // prove this\n \\valid // expected validation result \n }\n}\n\n// instantiations\n\n( instantiation \n (formula \"alt def of ⇒\") // abc = formula's label\n ((P A) (Q B)) // the metavar assignments\n (result \"valid\") // this instantiationshould succeed\n)\n\n//\n// incorrect variants\n//\n\n// no such formula\n( instantiation \n (formula \"Stewart's Theorem\") \n ((P A) (Q B)) \n (result \"invalid\") \n (reason \"no such formula\")\n)\n\n// bound, so not a metavariable\n( instantiation \n (formula \"alt def of ⇒\") \n ((P A) (Q B) (or A)) \n (result \"invalid\") \n (reason \"not a metavariable: or\")\n)\n\n// extraneous metavariable\n( instantiation \n (formula \"alt def of ⇒\") \n ((P A) (Q B) (R A))\n (result \"invalid\") \n (reason \"not a metavariable: R\")\n)\n\n// missing metavariable\n( instantiation \n (formula \"alt def of ⇒\") \n ( (Q B) )\n (result \"invalid\") \n (reason \"uninstantiated metavariable: P\")\n)\n\n// missing metavariable\n( instantiation \n (formula \"alt def of ⇒\") \n ( (P A) )\n (result \"invalid\") \n (reason \"uninstantiated metavariable: Q\")\n)\n"
},
{
"filename": "/validation tests/formula test 02.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "formula",
"description": "A valid instantiation, but the formula is inaccessible (and meaningless)."
}
},
"content": "\n// document\n\n(⇒ ¬ or),{ \n { \n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n } // the formula is accidentially inaccessible\n // start a proof\n { \n :(⇒ A B) \n (or (¬ A) B) \\invalid\n }\n}\n\n// instantiation\n\n( instantiation \n (formula \"alt def of ⇒\") \n ((P A) (Q B)) \n (result \"valid\") \n)\n"
},
{
"filename": "/validation tests/formula test 03.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "formula",
"description": "A valid instantiation, but not the one needed to justify the conclusion."
}
},
"content": "\n// document\n\n(⇒ ¬ or),{ \n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n // start a proof\n { \n :(⇒ A B) \n (or (¬ A) B) \\invalid\n }\n}\n\n// instantiation\n\n( instantiation \n (formula \"alt def of ⇒\") \n ((P A) (Q A)) \n (result \"valid\") \n)\n"
},
{
"filename": "/validation tests/formula test 04.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "formula",
"description": "Citing the wrong formula can false flag the cause of the error."
}
},
"content": "\n// document\n\n(⇒ ¬ or),{ \n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n :{ (⇒ P P) } \\label{reflexive of ⇒}\n // start a proof\n { \n :(⇒ A B) \n (or (¬ A) B) \\invalid\n }\n}\n\n// instantiation\n\n( instantiation\n (formula \"reflexive of ⇒\") \n ((P A) (Q B)) \n (result \"invalid\")\n (reason \"not a metavariable: Q\")\n)\n"
},
{
"filename": "/validation tests/formula test 05.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "formula",
"description": "A valid instantiation, but the formula is inaccessible."
}
},
"content": "\n// document\n\n(⇒ ¬ or),{ \n // start a proof\n { \n :(⇒ A B) \n (or (¬ A) B) \\invalid\n } \n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒} // too late\n}\n\n// instantiation\n\n( instantiation \n (formula \"alt def of ⇒\") \n ((P A) (Q B)) \n (result \"valid\") \n)\n"
},
{
"filename": "/validation tests/formula test 06.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "formula",
"description": "Natural Deduction Propositional Proof of (P⇒P)"
}
},
"content": "\n// document\n\n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{ \n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇔ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // Theorem (notice we get this for free .. we don't even need the proof)\n (⇒ P P ) \\valid\n \n // Baby warm up proof... just for kicks\n {\n { :P \n P \\valid \n }\n (⇒ P P ) \\valid \n }\n \n}\n\n// instantiation\n\n( instantiation // :{ :{:P P} (⇒ P P) }\n (formula \"⇒+\") \n ((W P) (V P)) \n (result \"valid\") \n)\n"
},
{
"filename": "/validation tests/formula test 07.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "formula",
"description": "Natural Deduction Propositional Proof (alt or-)"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇔ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n \n // Theorem (alt or-)\n { :(∨ P Q) :(¬ Q) P \\valid } // once again, we get it free from the \n // instantiations. No proof below needed!\n // But the proof below motivates the\n // instantiations\n\n // Altertnate or- proof (not needed but motivates the instantiations\n {\n { :(∨ P Q) \n :(¬ Q)\n { :P\n P \\valid // no instantiation needed\n }\n { :Q\n { :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\valid // motivates ¬- instantiation\n }\n P \\valid // motivates or- instantiation\n }\n } \n}\n\n\n// instantiation\n\n( instantiation // :{ :{ :(¬ P) Q (¬ Q)} P }\n (formula \"¬-\") \n ((W P) (V Q)) \n (result \"valid\") \n)\n\n( instantiation // :{ :(∨ P Q) :{ :P P } :{:Q P} P }\n (formula \"∨-\") \n ((W P) (V Q) (U P) ) \n (result \"valid\") \n)\n\n"
},
{
"filename": "/validation tests/formula test 08.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "formula",
"description": "Natural Deduction proof using the Identity Instantiation. So only one of the instantiations in the previous test should be needed."
}
},
"content": "\n// document\n\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{ \n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇔ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // Theorem\n { :(∨ W V) :(¬ V) W \\valid } \n \n // Altertnate or- proof\n {\n { :(∨ W V) :(¬ V)\n { :W\n W \\valid\n }\n { :V\n { :(¬ W)\n (¬ V) \\valid\n }\n W \\valid\n }\n W \\valid\n }\n }\n}\n\n// instantiation\n\n( instantiation // :{ :(∨ W V) :{ :W W } :{:V W} W }\n (formula \"∨-\") \n ((W W) (V V) (U W) ) \n (result \"valid\") \n)"
},
{
"filename": "/validation tests/formula test 09.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "formula",
"description": "Testing Pierce."
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{ \n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇔ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n // Theorem (Pierce) \n { (⇒ (⇒ (⇒ P Q) P) P) \\valid } \n\n // proof\n { \n { :(⇒ (⇒ P Q) P)\n { :(¬ P)\n { :P\n Q \\valid // motivates ¬-\n } \n (⇒ P Q) \\valid // motivates ⇒+\n P \\valid // motivates ⇒-\n }\n P \\valid // motivates second ¬- \n }\n (⇒ (⇒ (⇒ P Q) P) P) \\valid // motivates second ⇒+\n }\n \n}\n\n( instantiation // :{ :{:(¬ Q) P (¬ P)} Q }\n (formula \"¬-\")\n ((W Q) (V P))\n (result \"valid\")\n)\n\n( instantiation // :{ :{:P Q} (⇒ P Q ) }\n (formula \"⇒+\")\n ((W P) (V Q) )\n (result \"valid\")\n)\n\n( instantiation // :{ :(⇒ P Q) :(⇒ (⇒ P Q) P) P }\n (formula \"⇒-\")\n ((W (⇒ P Q)) (V P) )\n (result \"valid\")\n)\n\n( instantiation // :{ :{(¬ P) P (¬ P)} P }\n (formula \"¬-\")\n ((W P) (V P) )\n (result \"valid\")\n)\n\n( instantiation // :{ :(⇒ (⇒ P Q) P) P } (⇒ (⇒ (⇒ P Q) P) P) }\n (formula \"⇒+\")\n ((W (⇒ (⇒ P Q) P)) (V P) )\n (result \"valid\")\n)\n"
},
{
"filename": "/validation tests/formula test 10.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "formula",
"description": "Natural Deduction - extra instantiations don't hurt"
}
},
"content": "\n// document\n\n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{ \n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇔ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // Theorem (notice we get this for free .. we don't even need the proof)\n (⇒ P P ) \\valid\n \n // Baby warm up proof... just for kicks\n {\n { :P \n P \\valid \n }\n (⇒ P P ) \\valid \n }\n \n}\n\n// instantiation\n\n( instantiation // :{ :{:P P} (⇒ P P) }\n (formula \"⇒+\") \n ((W P) (V P)) \n (result \"valid\") \n)\n\n( instantiation // :{ :Z :Q (∧ Z Q) }\n (formula \"∧+\") \n ((W Z) (V Q)) \n (result \"valid\") \n)\n\n"
},
{
"filename": "/validation tests/formula test 11.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "formula",
"description": "ND using a Theorem as a Formula"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇔ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n // Theorem (alt or-)\n { :(∨ P Q) :(¬ Q) P \\valid } \\label{alt or-} // motivates or- instantiation\n\n // Alternate or- proof (not needed but motivates the instantiations\n {\n { :(∨ P Q) \n :(¬ Q)\n { :P\n P \\valid // no instantiation needed\n }\n { :Q\n { :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\valid // motivates ¬- instantiation\n }\n P \\valid // follows from the theorem\n }\n }\n \n // Corollary: (follows from the instantiated theorem)\n { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) \\valid } \n}\n\n\n// instantiations\n\n( instantiation // :{ :{ :(¬ P) Q (¬ Q)} P }\n (formula \"¬-\") \n ((W P) (V Q)) \n (result \"valid\") \n)\n\n( instantiation // :{ :(∨ P Q) :{ :P P } :{:Q P} P }\n (formula \"∨-\") \n ((W P) (V Q) (U P) ) \n (result \"valid\") \n)\n\n( instantiation // { :(∨ (⇒ A C) (∨ A B)) :(¬ (∨ A B)) (⇒ A C) }\n (formula \"alt or-\") \n ((P (⇒ A C)) (Q (∨ A B)) ) \n (result \"valid\") \n)\n"
},
{
"filename": "/validation tests/formula test 12.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "formula",
"description": "ND using a Theorem as a Formula"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇔ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n // Corollary: (should be invalid here)\n { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) \\invalid } \n \n // Theorem (alt or-)\n { :(∨ P Q) :(¬ Q) P \\valid } \\label{alt or-}\n\n // Alternate or- proof (not needed but motivates the instantiations\n {\n { :(∨ P Q) \n :(¬ Q)\n { :P\n P \\valid // no instantiation needed\n }\n { :Q\n { :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\valid // motivates ¬- instantiation\n }\n P \\valid // motivates or- instantiation\n }\n }\n \n}\n\n\n// instantiations\n\n( instantiation // :{ :{ :(¬ P) Q (¬ Q)} P }\n (formula \"¬-\") \n ((W P) (V Q)) \n (result \"valid\") \n)\n\n( instantiation // :{ :(∨ P Q) :{ :P P } :{:Q P} P }\n (formula \"∨-\") \n ((W P) (V Q) (U P) ) \n (result \"valid\") \n)\n\n( instantiation // { :(∨ (⇒ A C) (∨ A B)) :(¬ (∨ A B)) (⇒ A C) }\n (formula \"alt or-\") \n ((P (⇒ A C)) (Q (∨ A B)) ) \n (result \"valid\") \n)\n"
},
{
"filename": "/validation tests/instantiation hint 01.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "instantiation hint loop",
"passes": 2,
"description": "A basic test of the instantiation hint loop."
}
},
"content": "\n(⇒ ¬ or),{\n // some formulas\n :{ :(⇒ W V) :(⇒ V W) (⇔ W V) } // ⇔+\n :{ :(⇔ W V) (⇒ V W) (⇒ W V) } // ⇔-\n\n // Theorem\n { :(⇔ A B) (⇔ B A) }\n \n // a proof in 'since' form\n { :(⇔ A B) \n \n }\n}\n"
},
{
"filename": "/validation tests/instantiation hint 02.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "instantiation hint loop",
"description": "ND using a Theorem as a Formula"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n \n // Theorem (alt or-) (needs two passes to validate)\n // Fix errors in WIH 11 before testing this\n { :(∨ P Q) :(¬ Q) P } \\label{alt or-}\n\n // Alternate or- proof\n {\n :(∨ P Q) \n :(¬ Q)\n {\n :P\n P \\valid // no instantiation needed\n }\n {\n :Q\n {\n :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\valid // should instantiate ¬-\n }\n P \\valid // follows from the theorem \n }\n \n // Corollary: \n // Q: why does commenting this next line out create a mismatched grouper\n // error in the test in WIH 11? Does it cause it here too?\n { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) \\ref{alt or-} \\valid } \n\n}"
},
{
"filename": "/validation tests/strong instantiation hint 01.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "strong instantiation hint",
"description": "Basic test of a strong instantiation hint."
}
},
"content": "\n(⇒ ¬ or),{\n\n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n \n // start a proof\n { \n :(⇒ A B)\n (or (¬ A) B) \\valid\n }\n}\n"
},
{
"filename": "/validation tests/strong instantiation hint 02.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "strong instantiation hint",
"description": "A valid instantiation, but the formula is inaccessible (and meaningless)."
}
},
"content": "\n(⇒ ¬ or),{\n {\n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n }\n\n // start a proof\n { \n :(⇒ A B)\n (or (¬ A) B) \\invalid\n }\n}\n"
},
{
"filename": "/validation tests/strong instantiation hint 03.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "strong instantiation hint",
"description": "A valid instantiation, but not the one needed to justify the conclusion. But it finds the correct one anyway."
}
},
"content": "\n(⇒ ¬ or),{\n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n \n // simulating a blatant instantiation hint as a strong instantiation hint\n { :(⇒ A A) (or (¬ A) A) \\valid }\n\n // start a proof\n { \n :(⇒ A B)\n (or (¬ A) B) \\valid\n }\n}\n"
},
{
"filename": "/validation tests/strong instantiation hint 04.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "strong instantiation hint",
"description": "More than one formula to choose from."
}
},
"content": "\n(⇒ ¬ or),{\n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n :{ (⇒ P P) } \\label{reflexive of ⇒}\n\n // start a proof\n { \n :(⇒ A B) \n (or (¬ A) B) \\valid\n }\n}\n"
},
{
"filename": "/validation tests/strong instantiation hint 05.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "strong instantiation hint",
"description": "A valid instantiation, but the formula is inaccessible."
}
},
"content": "\n(⇒ ¬ or),{\n \n { \n :(⇒ A B) \n (or (¬ A) B) \\invalid\n } \n \n // too late\n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n}\n"
},
{
"filename": "/validation tests/strong instantiation hint 06.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "strong instantiation hint",
"description": "Natural Deduction Propositional Proof of (P⇒P)"
}
},
"content": "\n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // Theorem (because the premise is trivial, this will STILL validate)\n { (⇒ P P ) \\valid }\n \n // Baby warm up proof... just for kicks\n {\n {\n :P \n P \\valid // no justification needed\n }\n (⇒ P P ) \\valid // follows from theorem\n }\n \n}\n"
},
{
"filename": "/validation tests/strong instantiation hint 07.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "strong instantiation hint",
"description": "Natural Deduction Propositional Proof (alt or-)"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // Theorem (alt or-)\n // { :(∨ P Q) :(¬ Q) P \\valid } // this would not validate here\n\n // Altertnate or- proof (not needed but motivates the instantiations\n {\n :(∨ P Q) \n :(¬ Q)\n {\n :P\n P \\valid // no instantiation needed\n }\n {\n :Q\n {\n :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\valid // should instantiate ¬-\n }\n P \\valid // should instantiate ∨-\n }\n\n}\n"
},
{
"filename": "/validation tests/strong instantiation hint 08.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "strong instantiation hint",
"description": "Natural Deduction proof using the Identity Instantiation. So only one of the instantiations in the previous test should be needed."
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // Theorem\n // { :(∨ W V) :(¬ V) W \\valid } // this would not validate\n\n // Altertnate or- proof\n {\n {\n :(∨ W V) :(¬ V)\n {\n :W\n W \\valid\n }\n {\n :V\n {\n :(¬ W)\n (¬ V) \\valid\n }\n W \\valid\n }\n W \\valid // should instantiate ∨-\n }\n }\n}\n"
},
{
"filename": "/validation tests/strong instantiation hint 09.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "strong instantiation hint",
"description": "Testing Pierce."
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // Theorem (Pierce) \n // { (⇒ (⇒ (⇒ P Q) P) P) \\valid } // this would not validate\n\n // proof\n { \n {\n :(⇒ (⇒ P Q) P)\n {\n :(¬ P)\n {\n :P\n Q \\valid // should instantiate ¬-\n }\n (⇒ P Q) \\valid // should instantiate ⇒+\n P \\valid // should instantiate ⇒-\n }\n P \\valid // should instantiate ¬-\n }\n (⇒ (⇒ (⇒ P Q) P) P) \\valid // should instantiate ⇒+\n }\n\n}\n"
},
{
"filename": "/validation tests/strong instantiation hint 10.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "strong instantiation hint",
"description": "Natural Deduction - extra instantiations don't hurt"
}
},
"content": "\n// document\n\n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // extraneous\n { :{:Z V} (⇒ Z V) \\valid } // should instantiate ⇒+\n { :Z :Q (∧ Z Q) \\valid } // should instantiate ∧+\n\n // Theorem \n // (⇒ P P) \\valid // this would not validate\n \n // Baby warm up proof... just for kicks\n {\n {\n :P \n P \\valid \n }\n (⇒ P P ) \\valid // should instantiate ⇒+\n }\n\n}\n"
},
{
"filename": "/validation tests/strong instantiation hint 11.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "strong instantiation hint",
"description": "ND using a Theorem as a Formula"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n \n // Theorem (alt or-) (needs two passes to validate)\n // Fix errors in WIH 11 before testing this\n { :(∨ P Q) :(¬ Q) P \\invalid } \\label{alt or-}\n\n // Alternate or- proof\n {\n :(∨ P Q) \n :(¬ Q)\n {\n :P\n P \\valid // no instantiation needed\n }\n {\n :Q\n {\n :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\valid // should instantiate ¬-\n }\n P \\valid // follows from the theorem \n }\n \n // Corollary: \n // { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) ref{alt or-} valid } \n\n}"
},
{
"filename": "/validation tests/strong instantiation hint 12.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "strong instantiation hint",
"description": "ND using a Theorem as a Formula"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n // Corollary: (should be invalid here)\n { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) \\invalid } \n \n // Theorem (alt or-)\n // { :(∨ P Q) :(¬ Q) P \\valid } \\label{alt or-} // this would not validate\n\n // Alternate or- proof\n {\n :(∨ P Q) \n :(¬ Q)\n {\n :P\n P \\valid // no instantiation needed\n }\n {\n :Q\n {\n :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\valid // should instantiate ¬- \n }\n P \\valid // should instantiate ∨- \n }\n\n // Corollary: (follows from incorrect corollary above)\n { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) \\valid } \n\n}\n"
},
{
"filename": "/validation tests/strong instantiation hint 13.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "strong instantiation hint",
"description": "ND using a Theorem as a Formula"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n // Theorem (alt or-)\n // { :(∨ P Q) :(¬ Q) P \\valid } \\label{alt or-} // this would not validate\n\n // Alternate or- proof\n {\n :(∨ P Q) \n :(¬ Q)\n {\n :P\n P \\valid // no instantiation needed\n }\n {\n :Q\n {\n :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\valid // should instantiate ¬- \n }\n P \\valid // should instantiate ∨- \n }\n\n // Corollary: (follows from an instantation of the proof itself\n { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) \\valid } \n\n}\n"
},
{
"filename": "/validation tests/weak instantiation hint 01.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "weak instantiation hint",
"description": "Basic test of a weak instantiation hint."
}
},
"content": "\n(⇒ ¬ or),{\n\n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n \n // start a proof\n { \n :(⇒ A B)\n (or (¬ A) B) \\ref{alt def of ⇒} \\valid\n }\n}\n"
},
{
"filename": "/validation tests/weak instantiation hint 02.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "weak instantiation hint",
"description": "A valid instantiation, but the formula is inaccessible (and meaningless)."
}
},
"content": "\n(⇒ ¬ or),{\n {\n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n }\n\n // start a proof\n { \n :(⇒ A B)\n (or (¬ A) B) \\ref{alt def of ⇒} \\invalid\n }\n}\n"
},
{
"filename": "/validation tests/weak instantiation hint 03.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "weak instantiation hint",
"description": "A valid instantiation, but not the one needed to justify the conclusion."
}
},
"content": "\n(⇒ ¬ or),{\n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n \n // simulating a blatant instantiation hint as a weak instantiation hint\n {\n :(⇒ A A) (or (¬ A) A) \\ref{alt def of ⇒}\n \\valid\n }\n\n // start a proof\n { \n :(⇒ A B)\n (or (¬ A) B) \\invalid\n }\n}\n"
},
{
"filename": "/validation tests/weak instantiation hint 04.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "weak instantiation hint",
"description": "Citing the wrong formula."
}
},
"content": "\n(⇒ ¬ or),{\n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n :{ (⇒ P P) } \\label{reflexive of ⇒}\n\n // start a proof\n { \n :(⇒ A B) \n (or (¬ A) B) \\ref{reflexive of ⇒} \\invalid\n }\n}\n"
},
{
"filename": "/validation tests/weak instantiation hint 05.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "weak instantiation hint",
"description": "A valid instantiation, but the formula is inaccessible."
}
},
"content": "\n(⇒ ¬ or),{\n \n { \n :(⇒ A B) \n (or (¬ A) B) \\ref{reflexive of ⇒} \\invalid\n } \n \n // too late\n :{ :(⇒ P Q) (or (¬ P) Q) } \\label{alt def of ⇒}\n}\n"
},
{
"filename": "/validation tests/weak instantiation hint 06.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "weak instantiation hint",
"description": "Natural Deduction Propositional Proof of (P⇒P)"
}
},
"content": "\n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // Theorem (note this will STILL validate)\n { (⇒ P P ) \\ref{⇒+} \\valid }\n \n // Baby warm up proof... just for kicks\n {\n {\n :P \n P \\valid \n }\n (⇒ P P ) \\valid\n }\n \n}\n"
},
{
"filename": "/validation tests/weak instantiation hint 07.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "weak instantiation hint",
"description": "Natural Deduction Propositional Proof (alt or-)"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // Theorem (alt or-)\n // { :(∨ P Q) :(¬ Q) P \\valid } // this would not validate here\n\n // Altertnate or- proof (not needed but motivates the instantiations\n {\n {\n :(∨ P Q) \n :(¬ Q)\n {\n :P\n P \\valid // no instantiation needed\n }\n {\n :Q\n {\n :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\ref{¬-} \\valid\n }\n P \\ref{∨-} \\valid\n }\n }\n}\n"
},
{
"filename": "/validation tests/weak instantiation hint 08.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "weak instantiation hint",
"description": "Natural Deduction proof using the Identity Instantiation. So only one of the instantiations in the previous test should be needed."
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // Theorem\n // { :(∨ W V) :(¬ V) W \\valid } // this would not validate\n\n // Altertnate or- proof\n {\n {\n :(∨ W V) :(¬ V)\n {\n :W\n W \\valid\n }\n {\n :V\n {\n :(¬ W)\n (¬ V) \\valid\n }\n W \\valid\n }\n W \\ref{∨-} \\valid\n }\n }\n}\n"
},
{
"filename": "/validation tests/weak instantiation hint 09.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "weak instantiation hint",
"description": "Testing Pierce."
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // Theorem (Pierce) \n // { (⇒ (⇒ (⇒ P Q) P) P) \\valid } // this would not validate\n\n // proof\n { \n {\n :(⇒ (⇒ P Q) P)\n {\n :(¬ P)\n {\n :P\n Q \\ref{¬-} \\valid\n }\n (⇒ P Q) \\ref{⇒+} \\valid\n P \\ref{⇒-} \\valid\n }\n P \\ref{¬-} \\valid\n }\n (⇒ (⇒ (⇒ P Q) P) P) \\ref{⇒+} \\valid\n }\n\n}\n"
},
{
"filename": "/validation tests/weak instantiation hint 10.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "weak instantiation hint",
"description": "Natural Deduction - extra instantiations don't hurt"
}
},
"content": "\n// document\n\n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n\n // extraneous\n { :{:Z V} (⇒ Z V) \\ref{⇒+} \\valid }\n { :Z :Q (∧ Z Q) \\ref{∧+} \\valid }\n\n // Theorem \n // (⇒ P P) \\valid // this would not validate\n \n // Baby warm up proof... just for kicks\n {\n {\n :P \n P \\valid \n }\n (⇒ P P ) \\ref{⇒+} \\valid\n }\n\n}\n"
},
{
"filename": "/validation tests/weak instantiation hint 11.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "weak instantiation hint",
"description": "ND using a Theorem as a Formula"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n \n // Theorem (alt or-) (needs two passes to validate)\n // Q: why does including a #valid or #invalid tag after P throw an error?\n { :(∨ P Q) :(¬ Q) P \\invalid \\ref{∨-} } \\label{alt or-}\n\n // Alternate or- proof\n {\n :(∨ P Q) \n :(¬ Q)\n {\n :P\n P \\valid // no instantiation needed\n }\n {\n :Q\n {\n :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\ref{¬-} \\valid \n }\n P \\valid // follows from the theorem \n }\n \n // Corollary: \n // { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) #ref{alt or-} #valid } \n\n}"
},
{
"filename": "/validation tests/weak instantiation hint 12.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "weak instantiation hint",
"description": "ND using a Theorem as a Formula"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n // Corollary: (should be invalid here)\n { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) \\invalid } \n \n // Theorem (alt or-)\n // { :(∨ P Q) :(¬ Q) P #valid } #label{alt or-} // this would not validate\n\n // Alternate or- proof\n {\n :(∨ P Q) \n :(¬ Q)\n {\n :P\n P \\valid // no instantiation needed\n }\n {\n :Q\n {\n :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\ref{¬-} \\valid \n }\n P \\ref{∨-} \\valid \n }\n\n\n // Corollary: (follows from incorrect corollary above)\n { :(¬ (∨ A B)) :(∨ (⇒ A C) (∨ A B)) (⇒ A C) \\valid } \n\n}\n"
},
{
"filename": "/validation tests/weak instantiation hint 13.smackdown",
"metadata": {
"testing": {
"type": "validation",
"subtype": "weak instantiation hint",
"description": "ND using a Theorem as a Formula"
}
},
"content": "\n// global constants \n(∧ ∨ ⇒ ⇔ ¬ ∀ ∃ =),{\n\n // ND Prop rule library\n :{ :W :V (∧ W V) } \\label{∧+}\n :{ :(∧ W V) W V } \\label{∧-}\n :{ :W (∨ W V) (∨ V W) } \\label{∨+}\n :{ :(∨ W V) :{:W U} :{:V U} U } \\label{∨-}\n :{ :{:W V} (⇒ W V) } \\label{⇒+}\n :{ :W :(⇒ W V) V } \\label{⇒-}\n :{ :{:W V} :{:V W} (⇒ W V) } \\label{⇔+}\n :{ :(⇔ W V) {:W V} {:V W} } \\label{⇔-}\n :{ :{:W V (¬ V)} (¬ W) } \\label{¬+}\n :{ :{:(¬ W) V (¬ V)} W } \\label{¬-}\n \n // Theorem (alt or-)\n // { :(∨ P Q) :(¬ Q) P #valid } #label{alt or-} // this would not validate\n\n // Alternate or- proof\n {\n :(∨ P Q) \n :(¬ Q)\n {\n :P\n P \\valid // no instantiation needed\n }\n {\n :Q\n {\n :(¬ P)\n (¬ Q) \\valid // no instantiation needed\n }\n P \\ref{¬-} \\valid \n }\n P \\ref{∨-} \\valid \n } \\label{the proof}\n \n // Corollary: (follows from an instantation of the proof itself\n // Q: Why can't we cite #ref{proof} #valid on the following conclusion?\n { :(∨ (⇒ A C) (∨ A B)) :(¬ (∨ A B)) (⇒ A C) \\ref{the proof} \\valid } \n\n}\n"
}
]
// This file is a footer that will be embedded within /src/database.js when
// that file is regenerated using the "npm run build-db" command, as
// documented in /src/database/generate.js.
/**
* The testing database is built from a hierarchy of folders in the source
* code repository, containing `.putdown` and `.smackdown` files. The
* functions in this namespace are for querying that database. They are used
* in some of our testing suite, so that a library of large expressions, even
* large proofs, can be created outside of code, and just loaded from disk.
*
* The documentation of each function below assumes you have imported the
* database using the code `import Database from '/path/to/database.js'`.
* For example, importing it from a script in the `/tests` folder would use
* `import Database from '../src/database.js'`. Thus when the identifier
* `Database` appears in the documentation below, it is referring to the
* database module itself, as documented in this namespace.
*
* The source code file `database.js` is not intended to be imported into
* application code with the LDE itself, because it contains a large block of
* JSON in the code itself that is the entire contents of the database; that
* would significantly bloat the size of any app that used the LDE. However,
* that file is available for use in all of our testing scripts, and it is very
* useful in that regard.
*
* @namespace Database
*/
// The features added by this file are various querying conveniences for the
// database, which include conversion of putdown notation to LogicConcept
// instances and smackdown notation to MathConcept instances. For that, we
// need the relevant classes.
import { LogicConcept } from './logic-concept.js'
import { MathConcept } from './math-concept.js'
/**
* Each entry in the database has a unique name by which it is identified, and
* we call those names "keys." You can get a list of all keys using this
* function.
*
* The keys are simply the paths in the filesystem from which the data was
* loaded. So you might get a response of the form
* `['/folder1/file1.putdown','/folder2/subfolder/file2.smackdown']` and so on,
* containing as many files as there are in the database. If you think of the
* database as a filesystem, this function is like a recursive directory
* listing, filtering for only the `.putdown` and `.smackdown` files.
*
* @returns {string[]} all keys in the database
* @see {@link Database.keysStartingWith keysStartingWith()}
* @see {@link Database.keysPaths keysPaths()}
* @memberof Database
* @alias Database.keys
*/
export const keys = () =>
testingDatabase.map( entry => entry.filename )
/**
* This is a convenience function that returns just those keys in the database
* that begin with a certain prefix. You can use this to get all files
* recursively beneath a certain folder, for example, with a call like
* `Database.keysStartingWith('/my/folder/name/')`.
*
* @param {string} prefix - the prefix by which to filter
* @returns {string[]} all keys in the database that begin with the given
* prefix
* @see {@link Database.keys keys()}
* @see {@link Database.keysPaths keysPaths()}
* @memberof Database
* @alias Database.keysStartingWith
*/
export const keysStartingWith = prefix =>
keys().filter( key => key.startsWith( prefix ) )
/**
* Since the keys in the database are file paths, we might want to ask for the
* list of files inside a certain folder. We can do so recursively with
* {@link Database.keysStartingWith keysStartingWith()}, but this function
* lets us do so non-recursively.
*
* For example, if we call `Database.keysPaths('/example')`, we might get a
* response like `['one','two','x.putdown']` if indeed there were three things
* in the `/example` folder, including subfolders `one` and `two` and a file
* `x.putdown`. If the database is viewed as a filesystem, this function is
* like a directory listing.
*
* @param {string} folder - the folder whose contents should be listed
* @returns {string[]} all subfolder names or filenames that sit within the
* given folder (or the empty list if there are none, or if the folder name
* was invalid)
* @see {@link Database.keys keys()}
* @see {@link Database.keysStartingWith keysStartingWith()}
* @memberof Database
* @alias Database.keysPaths
*/
export const keysPaths = ( folder = '' ) => {
if ( !folder.endsWith( '/' ) ) folder += '/'
return Array.from( new Set( keysStartingWith( folder ).map(
key => key.substring( folder.length ).split( '/' )[0] ) ) )
}
/**
* Get the list of all keys in the database that refer to entries whose
* metadata satisfies a given predicate. For details on metadata content,
* see {@link Database.getMetadata getMetadata()}.
*
* @param {function} predicate - a function that takes as input a JSON object
* containing the metadata for a database entry and returns a boolean
* @returns {string[]} an array of all keys in the database whose
* corresponding entries pass the test inherent in the given predicate,
* that is, the predicate returns true when run on their metadata
* @see {@link Database.getMetadata getMetadata()}
* @memberof Database
* @alias Database.filterByMetadata
*/
export const filterByMetadata = predicate =>
testingDatabase.filter( entry => predicate( entry.metadata ) )
.map( entry => entry.filename )
// Read attributes from database entries; internal module helper function.
const getEntryAttribute = ( entryName, attribute ) => {
const entry = testingDatabase.find( entry => entry.filename == entryName )
return entry ? entry[attribute] : undefined
}
// Set attributes on database entries; internal module helper function.
const setEntryAttribute = ( entryName, attribute, value ) => {
const entry = testingDatabase.find( entry => entry.filename == entryName )
if ( entry ) entry[attribute] = value
return value
}
/**
* Look up the metadata associated with a database entry. The result will be
* a JavaScript `Object` instance, as if produced by `JSON.parse()`, possibly
* the empty object `{}` if the entry had no metadata, or `undefined` if the
* given key is invalid.
*
* The metadata of any entry in the database is a JSON object extracted from
* the (optional) YAML header in the original `.putdown` or `.smackdown` file.
* It can contain any information the original author put there. For example,
* it might state that the contents of the file are (or are not) valid
* `.putdown` (or `.smackdown`) syntax, so that the file can be used for
* testing the putdown (or smackdown) parser. Or it might be used to include
* other `.putdown` or `.smackdown` files as headers. The list of uses for
* this metadata is intended to grow over time, and thus not be fully specified
* in advance.
*
* The object returned is the actual metadata stored in the database, not a
* copy, so altering it will alter the contents of the database in memory (but
* not on the filesystem).
*
* @param {string} key - the key for the entry to look up
* @returns {Object} a JSON object containing the metadata for the entry
* @see {@link Database.filterByMetadata filterByMetadata()}
* @see {@link Database.getCode getCode()}
* @memberof Database
* @alias Database.getMetadata
*/
export const getMetadata = key => getEntryAttribute( key, 'metadata' )
/**
* Look up the original code associated with a database entry, which will be in
* either putdown or smackdown notation. The result will a string containing
* whatever was in the original `.putdown` or `.smackdown` file on disk when
* the database was created, or `undefined` if the key is invalid.
*
* If the entry's metadata has an `"includes"` member, the database build
* process respects this and includes other `.putdown` or `.smackdown` files as
* headers within this one. The result of this function will include the full
* `.putdown` or `.smackdown` code for this entry, which includes any code that
* was imported using the `"includes"` member of the metadata. To get just the
* original code without the other included files, see
* {@link Database.getCodeWithoutIncludes getCodeWithoutIncludes()}.
*
* The return value includes only putdown or smackdown code, not the YAML
* header that was converted into metadata. To get access to that information,
* see * {@link Database.getMetadata getMetadata()}.
*
* The return value is just the code, not the actual objects signified by that
* code. To get access to those objects, see
* {@link Database.getObjects getObjects()}.
*
* @param {string} key - the key for the entry to look up
* @returns {string} the putdown or smackdown source code for the entry
* @see {@link Database.getCodeWithoutIncludes getCodeWithoutIncludes()}
* @see {@link Database.getMetadata getMetadata()}
* @see {@link Database.getObjects getObjects()}
* @memberof Database
* @alias Database.getCode
*/
export const getCode = key => getEntryAttribute( key, 'content' )
/**
* This function works exactly the same as
* {@link Database.getCode getCode()}, except that any code included
* from a separate file using the `"includes"` member of the metadata object
* will not be included here. Thus the return value from this function is
* always a terminal substring of the return value of
* {@link Database.getCode getCode()}.
*
* @param {string} key - the key for the entry to look up
* @returns {string} the putdown or smackdown source code for the entry
* @see {@link Database.getCode getCode()}
* @see {@link Database.getMetadata getMetadata()}
* @memberof Database
* @alias Database.getCodeWithoutIncludes
*/
export const getCodeWithoutIncludes = key => {
const original = getEntryAttribute( key, 'original' )
return typeof( original ) == 'undefined' ?
getEntryAttribute( key, 'content' ) : original
}
// Get a cached parsed result of the given entry's full putdown/smackdown
// source, if any exists yet in the database.
const getParsedResult = key => getEntryAttribute( key, 'parsed' )
// Store in the cache the parsed result of the given entry's putdown/smackdown
// source, overwriting any previous cache value if there was one.
const setParsedResult = ( key, result ) =>
setEntryAttribute( key, 'parsed', result )
/**
* This function works exactly the same as
* {@link Database.getCode getCode()}, with two exceptions.
*
* 1. In addition to fetching the putdown or smackdown code, it also
* interprets it if possible, yielding an array of {@link MathConcept
* MathConcepts} or {@link LogicConcept LogicConcepts} as the result.
* (Putdown notation produces {@link LogicConcept LogicConcepts} and
* smackdown notation produces {@link MathConcept MathConcepts}, although
* since every {@link LogicConcept LogicConcept} is a {@link MathConcept
* MathConcept}, smackdown notation may produce either type, but putdown
* notation always produces {@link LogicConcept LogicConcepts}.)
* 2. Such results are cached so that future calls to this function with the
* same arguments will return the exact same {@link MathConcept
* MathConcept} or {@link LogicConcept LogicConcepts} instances. In
* particular, this means that if you manipulate the copies you get, you
* are mainpulating the copies in the cache. If this is not what you want,
* make separate copies.
*
* If the putdown or smackdown code fetched for the entry is not valid, then
* this function will instead throw a parsing error. If the key is an invalid
* key for the database, this function will return undefined. If the file
* contains the putdown or smackdown code for zero actual objects (e.g., only
* whitespace and comments) then this function will return an empty array.
*
* If you know that there is only one object in the file, and you want to get
* it without bothering to do `getObjects(key)[0]`, you can just call
* {@link Database.getObject getObject()} instead.
*
* @param {string} key - the key for the entry to look up
* @returns {LogicConcept[]} the meaning of the putdown or smackdown source
* code for the entry, as an array of {@link MathConcept MathConcept} or
* {@link LogicConcept LogicConcept} instances
* @see {@link Database.getCode getCode()}
* @see {@link Database.getObject getObject()}
* @memberof Database
* @alias Database.getObjects
*/
export const getObjects = key => {
const cached = getParsedResult( key )
// if we cached a list of LCs, return them
if ( cached instanceof Array ) return cached
// if we cached something else, it was an error object; re-throw it
if ( cached ) throw cached
// we have no cache, so we must parse; get the putdown/smackdown code
const code = getCode( key )
// if we have no code, we cannot proceed
if ( !code ) return undefined
try {
// if we parse without error, cache the result and then return it
return setParsedResult( key,
key.endsWith( '.putdown' ) ? LogicConcept.fromPutdown( code )
: MathConcept.fromSmackdown( code ) )
} catch ( error ) {
// otherwise, cache the error and also throw it
throw setParsedResult( key, error )
}
}
/**
* This function works exactly the same as
* {@link Database.getObjects getObjects()}, with one exception:
* If the putdown or smackdown source code parses into an array of length one,
* this function just returns the sole entry of that array, but if instead the
* array has any other length, this function throws an error, whose message
* states that it expected an array of length one.
*
* @param {string} key - the key for the entry to look up
* @returns {LogicConcept} the meaning of the putdown or smackdown source code
* for the entry, as a single {@link MathConcept MathConcept} or
* {@link LogicConcept LogicConcept} instance
* @see {@link Database.getCode getCode()}
* @see {@link Database.getObjects getObjects()}
* @memberof Database
* @alias Database.getObject
*/
export const getObject = key => {
const all = getObjects( key )
if ( all.length != 1 )
throw `Expected 1 LogicConcept, got ${all.length}`
return all[0]
}
// create a default object so that clients can do:
// import Database from './database.js'
export default {
keys, keysStartingWith, keysPaths, filterByMetadata,
getMetadata, getCode, getCodeWithoutIncludes, getObjects, getObject
}
source